summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Tools/cnf_funcs.ML

changeset 32960 | 69916a850301 |

parent 32740 | 9dd0a2f83429 |

child 33035 | 15eab423e573 |

1.1 --- a/src/HOL/Tools/cnf_funcs.ML Sat Oct 17 01:05:59 2009 +0200 1.2 +++ b/src/HOL/Tools/cnf_funcs.ML Sat Oct 17 14:43:18 2009 +0200 1.3 @@ -2,33 +2,34 @@ 1.4 Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) 1.5 Author: Tjark Weber, TU Muenchen 1.6 1.7 - FIXME: major overlaps with the code in meson.ML 1.8 +FIXME: major overlaps with the code in meson.ML 1.9 + 1.10 +Functions and tactics to transform a formula into Conjunctive Normal 1.11 +Form (CNF). 1.12 1.13 - Description: 1.14 - This file contains functions and tactics to transform a formula into 1.15 - Conjunctive Normal Form (CNF). 1.16 - A formula in CNF is of the following form: 1.17 +A formula in CNF is of the following form: 1.18 1.19 - (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk) 1.20 - False 1.21 - True 1.22 + (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk) 1.23 + False 1.24 + True 1.25 1.26 - where each xij is a literal (a positive or negative atomic Boolean term), 1.27 - i.e. the formula is a conjunction of disjunctions of literals, or 1.28 - "False", or "True". 1.29 +where each xij is a literal (a positive or negative atomic Boolean 1.30 +term), i.e. the formula is a conjunction of disjunctions of literals, 1.31 +or "False", or "True". 1.32 1.33 - A (non-empty) disjunction of literals is referred to as "clause". 1.34 +A (non-empty) disjunction of literals is referred to as "clause". 1.35 1.36 - For the purpose of SAT proof reconstruction, we also make use of another 1.37 - representation of clauses, which we call the "raw clauses". 1.38 - Raw clauses are of the form 1.39 +For the purpose of SAT proof reconstruction, we also make use of 1.40 +another representation of clauses, which we call the "raw clauses". 1.41 +Raw clauses are of the form 1.42 + 1.43 + [..., x1', x2', ..., xn'] |- False , 1.44 1.45 - [..., x1', x2', ..., xn'] |- False , 1.46 +where each xi is a literal, and each xi' is the negation normal form 1.47 +of ~xi. 1.48 1.49 - where each xi is a literal, and each xi' is the negation normal form of ~xi. 1.50 - 1.51 - Literals are successively removed from the hyps of raw clauses by resolution 1.52 - during SAT proof reconstruction. 1.53 +Literals are successively removed from the hyps of raw clauses by 1.54 +resolution during SAT proof reconstruction. 1.55 *) 1.56 1.57 signature CNF =