(* Title: HOL/Tools/prop_logic.ML
ID: $Id$
Author: Tjark Weber
Copyright 2004-2005
Formulas of propositional logic.
*)
signature PROP_LOGIC =
sig
datatype prop_formula =
True
| False
| BoolVar of int (* NOTE: only use indices >= 1 *)
| Not of prop_formula
| Or of prop_formula * prop_formula
| And of prop_formula * prop_formula
val SNot : prop_formula -> prop_formula
val SOr : prop_formula * prop_formula -> prop_formula
val SAnd : prop_formula * prop_formula -> prop_formula
val simplify : prop_formula -> prop_formula (* eliminates True/False and double-negation *)
val indices : prop_formula -> int list (* set of all variable indices *)
val maxidx : prop_formula -> int (* maximal variable index *)
val exists : prop_formula list -> prop_formula (* finite disjunction *)
val all : prop_formula list -> prop_formula (* finite conjunction *)
val dot_product : prop_formula list * prop_formula list -> prop_formula
val is_nnf : prop_formula -> bool (* returns true iff the formula is in negation normal form *)
val is_cnf : prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *)
val nnf : prop_formula -> prop_formula (* negation normal form *)
val cnf : prop_formula -> prop_formula (* conjunctive normal form *)
val auxcnf : prop_formula -> prop_formula (* cnf with auxiliary variables *)
val defcnf : prop_formula -> prop_formula (* definitional cnf *)
val eval : (int -> bool) -> prop_formula -> bool (* semantics *)
(* propositional representation of HOL terms *)
val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
(* HOL term representation of propositional formulae *)
val term_of_prop_formula : prop_formula -> Term.term
end;
structure PropLogic : PROP_LOGIC =
struct
(* ------------------------------------------------------------------------- *)
(* prop_formula: formulas of propositional logic, built from Boolean *)
(* variables (referred to by index) and True/False using *)
(* not/or/and *)
(* ------------------------------------------------------------------------- *)
datatype prop_formula =
True
| False
| BoolVar of int (* NOTE: only use indices >= 1 *)
| Not of prop_formula
| Or of prop_formula * prop_formula
| And of prop_formula * prop_formula;
(* ------------------------------------------------------------------------- *)
(* The following constructor functions make sure that True and False do not *)
(* occur within any of the other connectives (i.e. Not, Or, And), and *)
(* perform double-negation elimination. *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
fun SNot True = False
| SNot False = True
| SNot (Not fm) = fm
| SNot fm = Not fm;
(* prop_formula * prop_formula -> prop_formula *)
fun SOr (True, _) = True
| SOr (_, True) = True
| SOr (False, fm) = fm
| SOr (fm, False) = fm
| SOr (fm1, fm2) = Or (fm1, fm2);
(* prop_formula * prop_formula -> prop_formula *)
fun SAnd (True, fm) = fm
| SAnd (fm, True) = fm
| SAnd (False, _) = False
| SAnd (_, False) = False
| SAnd (fm1, fm2) = And (fm1, fm2);
(* ------------------------------------------------------------------------- *)
(* simplify: eliminates True/False below other connectives, and double- *)
(* negation *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
fun simplify (Not fm) = SNot (simplify fm)
| simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2)
| simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
| simplify fm = fm;
(* ------------------------------------------------------------------------- *)
(* indices: collects all indices of Boolean variables that occur in a *)
(* propositional formula 'fm'; no duplicates *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> int list *)
fun indices True = []
| indices False = []
| indices (BoolVar i) = [i]
| indices (Not fm) = indices fm
| indices (Or (fm1, fm2)) = (indices fm1) union_int (indices fm2)
| indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
(* ------------------------------------------------------------------------- *)
(* maxidx: computes the maximal variable index occuring in a formula of *)
(* propositional logic 'fm'; 0 if 'fm' contains no variable *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> int *)
fun maxidx True = 0
| maxidx False = 0
| maxidx (BoolVar i) = i
| maxidx (Not fm) = maxidx fm
| maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2)
| maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
(* ------------------------------------------------------------------------- *)
(* exists: computes the disjunction over a list 'xs' of propositional *)
(* formulas *)
(* ------------------------------------------------------------------------- *)
(* prop_formula list -> prop_formula *)
fun exists xs = Library.foldl SOr (False, xs);
(* ------------------------------------------------------------------------- *)
(* all: computes the conjunction over a list 'xs' of propositional formulas *)
(* ------------------------------------------------------------------------- *)
(* prop_formula list -> prop_formula *)
fun all xs = Library.foldl SAnd (True, xs);
(* ------------------------------------------------------------------------- *)
(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *)
(* ------------------------------------------------------------------------- *)
(* prop_formula list * prop_formula list -> prop_formula *)
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
(* ------------------------------------------------------------------------- *)
(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e. *)
(* only variables may be negated, but not subformulas). *)
(* ------------------------------------------------------------------------- *)
local
fun is_literal (BoolVar _) = true
| is_literal (Not (BoolVar _)) = true
| is_literal _ = false
fun is_conj_disj (Or (fm1, fm2)) =
is_conj_disj fm1 andalso is_conj_disj fm2
| is_conj_disj (And (fm1, fm2)) =
is_conj_disj fm1 andalso is_conj_disj fm2
| is_conj_disj fm =
is_literal fm
in
fun is_nnf True = true
| is_nnf False = true
| is_nnf fm = is_conj_disj fm
end;
(* ------------------------------------------------------------------------- *)
(* is_cnf: returns 'true' iff the formula is in conjunctive normal form *)
(* (i.e. a conjunction of disjunctions). *)
(* ------------------------------------------------------------------------- *)
local
fun is_literal (BoolVar _) = true
| is_literal (Not (BoolVar _)) = true
| is_literal _ = false
fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2
| is_disj fm = is_literal fm
fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2
| is_conj fm = is_disj fm
in
fun is_cnf True = true
| is_cnf False = true
| is_cnf fm = is_conj fm
end;
(* ------------------------------------------------------------------------- *)
(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
(* logic (i.e. only variables may be negated, but not subformulas). *)
(* Simplification (c.f. 'simplify') is performed as well. *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
fun
(* constants *)
nnf True = True
| nnf False = False
(* variables *)
| nnf (BoolVar i) = (BoolVar i)
(* 'or' and 'and' as outermost connectives are left untouched *)
| nnf (Or (fm1, fm2)) = SOr (nnf fm1, nnf fm2)
| nnf (And (fm1, fm2)) = SAnd (nnf fm1, nnf fm2)
(* 'not' + constant *)
| nnf (Not True) = False
| nnf (Not False) = True
(* 'not' + variable *)
| nnf (Not (BoolVar i)) = Not (BoolVar i)
(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
| nnf (Not (Or (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
| nnf (Not (And (fm1, fm2))) = SOr (nnf (SNot fm1), nnf (SNot fm2))
(* double-negation elimination *)
| nnf (Not (Not fm)) = nnf fm;
(* ------------------------------------------------------------------------- *)
(* cnf: computes the conjunctive normal form (i.e. a conjunction of *)
(* disjunctions) of a formula 'fm' of propositional logic. The result *)
(* formula may be exponentially longer than 'fm'. *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
fun cnf fm =
let
fun
(* constants *)
cnf_from_nnf True = True
| cnf_from_nnf False = False
(* literals *)
| cnf_from_nnf (BoolVar i) = BoolVar i
| cnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *)
(* pushing 'or' inside of 'and' using distributive laws *)
| cnf_from_nnf (Or (fm1, fm2)) =
let
fun cnf_or (And (fm11, fm12), fm2) =
And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
| cnf_or (fm1, And (fm21, fm22)) =
And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
(* neither subformula contains 'and' *)
| cnf_or (fm1, fm2) =
Or (fm1, fm2)
in
cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
end
(* 'and' as outermost connective is left untouched *)
| cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
in
(cnf_from_nnf o nnf) fm
end;
(* ------------------------------------------------------------------------- *)
(* auxcnf: computes the definitional conjunctive normal form of a formula *)
(* 'fm' of propositional logic, introducing auxiliary variables if *)
(* necessary to avoid an exponential blowup of the formula. The result *)
(* formula is satisfiable if and only if 'fm' is satisfiable. *)
(* Auxiliary variables are introduced as switches for OR-nodes, based *)
(* on the observation that e.g. "fm1 OR (fm21 AND fm22)" is *)
(* equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR *)
(* aux)". *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than *)
(* 'defcnf' below, but sometimes generates much larger SAT problems *)
(* overall (hence it must sometimes generate longer clauses than *)
(* 'defcnf' does). It is currently not quite clear to me if one of the *)
(* algorithms is clearly superior to the other, but I suggest using *)
(* 'defcnf' instead. *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
fun auxcnf fm =
let
(* convert formula to NNF first *)
val fm' = nnf fm
(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
(* int ref *)
val new = ref (maxidx fm' + 1)
(* unit -> int *)
fun new_idx () = let val idx = !new in new := idx+1; idx end
(* prop_formula -> prop_formula *)
fun
(* constants *)
auxcnf_from_nnf True = True
| auxcnf_from_nnf False = False
(* literals *)
| auxcnf_from_nnf (BoolVar i) = BoolVar i
| auxcnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *)
(* pushing 'or' inside of 'and' using auxiliary variables *)
| auxcnf_from_nnf (Or (fm1, fm2)) =
let
val fm1' = auxcnf_from_nnf fm1
val fm2' = auxcnf_from_nnf fm2
(* prop_formula * prop_formula -> prop_formula *)
fun auxcnf_or (And (fm11, fm12), fm2) =
(case fm2 of
(* do not introduce an auxiliary variable for literals *)
BoolVar _ =>
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
| Not _ =>
And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
| _ =>
let
val aux = BoolVar (new_idx ())
in
And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
end)
| auxcnf_or (fm1, And (fm21, fm22)) =
(case fm1 of
(* do not introduce an auxiliary variable for literals *)
BoolVar _ =>
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
| Not _ =>
And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
| _ =>
let
val aux = BoolVar (new_idx ())
in
And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
end)
(* neither subformula contains 'and' *)
| auxcnf_or (fm1, fm2) =
Or (fm1, fm2)
in
auxcnf_or (fm1', fm2')
end
(* 'and' as outermost connective is left untouched *)
| auxcnf_from_nnf (And (fm1, fm2)) =
And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
in
auxcnf_from_nnf fm'
end;
(* ------------------------------------------------------------------------- *)
(* defcnf: computes the definitional conjunctive normal form of a formula *)
(* 'fm' of propositional logic, introducing auxiliary variables to *)
(* avoid an exponential blowup of the formula. The result formula is *)
(* satisfiable if and only if 'fm' is satisfiable. Auxiliary variables *)
(* are introduced as abbreviations for AND-, OR-, and NOT-nodes, based *)
(* on the following equisatisfiabilities (+/- indicates polarity): *)
(* LITERAL+ == LITERAL *)
(* LITERAL- == NOT LITERAL *)
(* (NOT fm1)+ == aux AND (NOT aux OR fm1-) *)
(* (fm1 OR fm2)+ == aux AND (NOT aux OR fm1+ OR fm2+) *)
(* (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+) *)
(* (NOT fm1)- == aux AND (NOT aux OR fm1+) *)
(* (fm1 OR fm2)- == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-) *)
(* (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-) *)
(* Example: *)
(* NOT (a AND b) == aux1 AND (NOT aux1 OR aux2) *)
(* AND (NOT aux2 OR NOT a OR NOT b) *)
(* ------------------------------------------------------------------------- *)
(* prop_formula -> prop_formula *)
fun defcnf fm =
if is_cnf fm then
fm
else let
(* simplify formula first *)
val fm' = simplify fm
(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
(* int ref *)
val new = ref (maxidx fm' + 1)
(* unit -> int *)
fun new_idx () = let val idx = !new in new := idx+1; idx end
(* optimization for n-ary disjunction/conjunction *)
(* prop_formula -> prop_formula list *)
fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
| disjuncts fm1 = [fm1]
(* prop_formula -> prop_formula list *)
fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
| conjuncts fm1 = [fm1]
(* polarity -> formula -> (defining clauses, literal) *)
(* bool -> prop_formula -> prop_formula * prop_formula *)
fun
(* constants *)
defcnf' true True = (True, True)
| defcnf' false True = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
| defcnf' true False = (True, False)
| defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
(* literals *)
| defcnf' true (BoolVar i) = (True, BoolVar i)
| defcnf' false (BoolVar i) = (True, Not (BoolVar i))
| defcnf' true (Not (BoolVar i)) = (True, Not (BoolVar i))
| defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
(* 'not' *)
| defcnf' polarity (Not fm1) =
let
val (def1, aux1) = defcnf' (not polarity) fm1
val aux = BoolVar (new_idx ())
val def = Or (Not aux, aux1)
in
(SAnd (def1, def), aux)
end
(* 'or' *)
| defcnf' polarity (Or (fm1, fm2)) =
let
val fms = disjuncts (Or (fm1, fm2))
val (defs, auxs) = split_list (map (defcnf' polarity) fms)
val aux = BoolVar (new_idx ())
val def = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
in
(SAnd (all defs, def), aux)
end
(* 'and' *)
| defcnf' polarity (And (fm1, fm2)) =
let
val fms = conjuncts (And (fm1, fm2))
val (defs, auxs) = split_list (map (defcnf' polarity) fms)
val aux = BoolVar (new_idx ())
val def = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
in
(SAnd (all defs, def), aux)
end
(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
(* prop_formula -> prop_formula * prop_formula *)
fun defcnf_or (Or (fm1, fm2)) =
let
val (def1, aux1) = defcnf_or fm1
val (def2, aux2) = defcnf_or fm2
in
(SAnd (def1, def2), Or (aux1, aux2))
end
| defcnf_or fm =
defcnf' true fm
(* prop_formula -> prop_formula * prop_formula *)
fun defcnf_and (And (fm1, fm2)) =
let
val (def1, aux1) = defcnf_and fm1
val (def2, aux2) = defcnf_and fm2
in
(SAnd (def1, def2), And (aux1, aux2))
end
| defcnf_and (Or (fm1, fm2)) =
let
val (def1, aux1) = defcnf_or fm1
val (def2, aux2) = defcnf_or fm2
in
(SAnd (def1, def2), Or (aux1, aux2))
end
| defcnf_and fm =
defcnf' true fm
in
SAnd (defcnf_and fm')
end;
(* ------------------------------------------------------------------------- *)
(* eval: given an assignment 'a' of Boolean values to variable indices, the *)
(* truth value of a propositional formula 'fm' is computed *)
(* ------------------------------------------------------------------------- *)
(* (int -> bool) -> prop_formula -> bool *)
fun eval a True = true
| eval a False = false
| eval a (BoolVar i) = (a i)
| eval a (Not fm) = not (eval a fm)
| eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2)
| eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
(* ------------------------------------------------------------------------- *)
(* prop_formula_of_term: returns the propositional structure of a HOL term, *)
(* with subterms replaced by Boolean variables. Also returns a table *)
(* of terms and corresponding variables that extends the table that was *)
(* given as an argument. Usually, you'll just want to use *)
(* 'Termtab.empty' as value for 'table'. *)
(* ------------------------------------------------------------------------- *)
(* Note: The implementation is somewhat optimized; the next index to be used *)
(* is computed only when it is actually needed. However, when *)
(* 'prop_formula_of_term' is invoked many times, it might be more *)
(* efficient to pass and return this value as an additional parameter, *)
(* so that it does not have to be recomputed (by folding over the *)
(* table) for each invocation. *)
(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
fun prop_formula_of_term t table =
let
val next_idx_is_valid = ref false
val next_idx = ref 0
fun get_next_idx () =
if !next_idx_is_valid then
inc next_idx
else (
next_idx := Termtab.fold (curry Int.max o snd) table 0;
next_idx_is_valid := true;
inc next_idx
)
fun aux (Const ("True", _)) table =
(True, table)
| aux (Const ("False", _)) table =
(False, table)
| aux (Const ("Not", _) $ x) table =
apfst Not (aux x table)
| aux (Const ("op |", _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
in
(Or (fm1, fm2), table2)
end
| aux (Const ("op &", _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
in
(And (fm1, fm2), table2)
end
| aux x table =
(case Termtab.lookup table x of
SOME i =>
(BoolVar i, table)
| NONE =>
let
val i = get_next_idx ()
in
(BoolVar i, Termtab.update (x, i) table)
end)
in
aux t table
end;
(* ------------------------------------------------------------------------- *)
(* term_of_prop_formula: returns a HOL term that corresponds to a *)
(* propositional formula, with Boolean variables replaced by Free's *)
(* ------------------------------------------------------------------------- *)
(* Note: A more generic implementation should take another argument of type *)
(* Term.term Inttab.table (or so) that specifies HOL terms for some *)
(* Boolean variables in the formula, similar to 'prop_formula_of_term' *)
(* (but the other way round). *)
(* prop_formula -> Term.term *)
fun term_of_prop_formula True =
HOLogic.true_const
| term_of_prop_formula False =
HOLogic.false_const
| term_of_prop_formula (BoolVar i) =
Free ("v" ^ Int.toString i, HOLogic.boolT)
| term_of_prop_formula (Not fm) =
HOLogic.mk_not (term_of_prop_formula fm)
| term_of_prop_formula (Or (fm1, fm2)) =
HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
| term_of_prop_formula (And (fm1, fm2)) =
HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
end;