1(* ========================================================================= *) 2(* FIRST-ORDER LOGIC CANONICALIZATION *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibCanon = 7sig 8 9type term = mlibTerm.term 10type formula = mlibTerm.formula 11 12(* Simplification *) 13val simplify : formula -> formula 14 15(* Negation normal form *) 16val nnf : formula -> formula 17 18(* Prenex normal form *) 19val prenex : formula -> formula 20val pnf : formula -> formula 21 22(* Skolemization *) 23val skolemize : formula -> formula 24val full_skolemize : formula -> formula 25 26(* A tautology filter for clauses *) 27val tautologous : formula list -> bool 28 29(* Conjunctive normal form *) 30val clausal : formula -> formula list list 31val purecnf : formula -> formula 32val cnf : formula -> formula (* simp + nnf + skolemize + purecnf *) 33val is_clause : formula -> bool 34val is_cnf : formula -> bool 35 36(* Categorizing sets of clauses *) 37datatype prop = Propositional | Effectively_propositional | Non_propositional 38datatype equal = Non_equality | Equality | Pure_equality 39datatype horn = Trivial | Unit | Both_horn | Horn | Negative_horn | Non_horn 40type category = {prop : prop, equal : equal, horn : horn} 41 42val categorize_clauses : formula list -> category 43val category_to_string : category -> string 44 45end 46