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