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