1(* ========================================================================= *)
2(* CLAUSE = ID + THEOREM                                                     *)
3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Clause =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* A type of clause.                                                         *)
11(* ------------------------------------------------------------------------- *)
12
13datatype literalOrder =
14    NoLiteralOrder
15  | UnsignedLiteralOrder
16  | PositiveLiteralOrder
17
18type parameters =
19     {ordering : KnuthBendixOrder.kbo,
20      orderLiterals : literalOrder,
21      orderTerms : bool}
22
23type clauseId = int
24
25type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm}
26
27type clause
28
29(* ------------------------------------------------------------------------- *)
30(* Basic operations.                                                         *)
31(* ------------------------------------------------------------------------- *)
32
33val default : parameters
34
35val newId : unit -> clauseId
36
37val mk : clauseInfo -> clause
38
39val dest : clause -> clauseInfo
40
41val id : clause -> clauseId
42
43val thm : clause -> Thm.thm
44
45val equalThms : clause -> clause -> bool
46
47val literals : clause -> Thm.clause
48
49val isTautology : clause -> bool
50
51val isContradiction : clause -> bool
52
53(* ------------------------------------------------------------------------- *)
54(* The term ordering is used to cut down inferences.                         *)
55(* ------------------------------------------------------------------------- *)
56
57val largestLiterals : clause -> LiteralSet.set
58
59val largestEquations :
60    clause -> (Literal.literal * Rewrite.orient * Term.term) list
61
62val largestSubterms :
63    clause -> (Literal.literal * Term.path * Term.term) list
64
65val allSubterms : clause -> (Literal.literal * Term.path * Term.term) list
66
67(* ------------------------------------------------------------------------- *)
68(* Subsumption.                                                              *)
69(* ------------------------------------------------------------------------- *)
70
71val subsumes : clause Subsume.subsume -> clause -> bool
72
73(* ------------------------------------------------------------------------- *)
74(* Simplifying rules: these preserve the clause id.                          *)
75(* ------------------------------------------------------------------------- *)
76
77val freshVars : clause -> clause
78
79val simplify : clause -> clause option
80
81val reduce : Units.units -> clause -> clause
82
83val rewrite : Rewrite.rewrite -> clause -> clause
84
85(* ------------------------------------------------------------------------- *)
86(* Inference rules: these generate new clause ids.                           *)
87(* ------------------------------------------------------------------------- *)
88
89val factor : clause -> clause list
90
91val resolve : clause * Literal.literal -> clause * Literal.literal -> clause
92
93val paramodulate :
94    clause * Literal.literal * Rewrite.orient * Term.term ->
95    clause * Literal.literal * Term.path * Term.term -> clause
96
97(* ------------------------------------------------------------------------- *)
98(* Pretty printing.                                                          *)
99(* ------------------------------------------------------------------------- *)
100
101val showId : bool ref
102
103val pp : clause Print.pp
104
105val toString : clause -> string
106
107end
108