--- a/src/HOL/Tools/cnf_funcs.ML Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Sat Oct 17 14:43:18 2009 +0200
@@ -2,33 +2,34 @@
Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
Author: Tjark Weber, TU Muenchen
- FIXME: major overlaps with the code in meson.ML
+FIXME: major overlaps with the code in meson.ML
+
+Functions and tactics to transform a formula into Conjunctive Normal
+Form (CNF).
- Description:
- This file contains functions and tactics to transform a formula into
- Conjunctive Normal Form (CNF).
- A formula in CNF is of the following form:
+A formula in CNF is of the following form:
- (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
- False
- True
+ (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
+ False
+ True
- where each xij is a literal (a positive or negative atomic Boolean term),
- i.e. the formula is a conjunction of disjunctions of literals, or
- "False", or "True".
+where each xij is a literal (a positive or negative atomic Boolean
+term), i.e. the formula is a conjunction of disjunctions of literals,
+or "False", or "True".
- A (non-empty) disjunction of literals is referred to as "clause".
+A (non-empty) disjunction of literals is referred to as "clause".
- For the purpose of SAT proof reconstruction, we also make use of another
- representation of clauses, which we call the "raw clauses".
- Raw clauses are of the form
+For the purpose of SAT proof reconstruction, we also make use of
+another representation of clauses, which we call the "raw clauses".
+Raw clauses are of the form
+
+ [..., x1', x2', ..., xn'] |- False ,
- [..., x1', x2', ..., xn'] |- False ,
+where each xi is a literal, and each xi' is the negation normal form
+of ~xi.
- where each xi is a literal, and each xi' is the negation normal form of ~xi.
-
- Literals are successively removed from the hyps of raw clauses by resolution
- during SAT proof reconstruction.
+Literals are successively removed from the hyps of raw clauses by
+resolution during SAT proof reconstruction.
*)
signature CNF =