| products/Sources/formale Sprachen/Isabelle/Tools/Metis/src/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Tptp.sig Sprache: Unknown
|
Spracherkennung für: .sig vermutete Sprache: Text {Text[129] Isabelle[145] Abap[155]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] (* ========================================================================= *) (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Rule = sig (* ------------------------------------------------------------------------- *) (* An equation consists of two terms (t,u) plus a theorem (stronger than) *) (* t = u \/ C. *) (* ------------------------------------------------------------------------- *) type equation = (Term.term * Term.term) * Thm.thm val ppEquation : equation Print.pp val equationToString : equation -> string (* Returns t = u if the equation theorem contains this literal *) val equationLiteral : equation -> Literal.literal option val reflEqn : Term.term -> equation val symEqn : equation -> equation val transEqn : equation -> equation -> equation (* ------------------------------------------------------------------------- *) (* A conversion takes a term t and either: *) (* 1. Returns a term u together with a theorem (stronger than) t = u \/ C. *) (* 2. Raises an Error exception. *) (* ------------------------------------------------------------------------- *) type conv = Term.term -> Term.term * Thm.thm val allConv : conv val noConv : conv val thenConv : conv -> conv -> conv val orelseConv : conv -> conv -> conv val tryConv : conv -> conv val repeatConv : conv -> conv val firstConv : conv list -> conv val everyConv : conv list -> conv val rewrConv : equation -> Term.path -> conv val pathConv : conv -> Term.path -> conv val subtermConv : conv -> int -> conv val subtermsConv : conv -> conv (* All function arguments *) (* ------------------------------------------------------------------------- *) (* Applying a conversion to every subterm, with some traversal strategy. *) (* ------------------------------------------------------------------------- *) val bottomUpConv : conv -> conv val topDownConv : conv -> conv val repeatTopDownConv : conv -> conv (* useful for rewriting *) (* ------------------------------------------------------------------------- *) (* A literule (bad pun) takes a literal L and either: *) (* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C. *) (* 2. Raises an Error exception. *) (* ------------------------------------------------------------------------- *) type literule = Literal.literal -> Literal.literal * Thm.thm val allLiterule : literule val noLiterule : literule val thenLiterule : literule -> literule -> literule val orelseLiterule : literule -> literule -> literule val tryLiterule : literule -> literule val repeatLiterule : literule -> literule val firstLiterule : literule list -> literule val everyLiterule : literule list -> literule val rewrLiterule : equation -> Term.path -> literule val pathLiterule : conv -> Term.path -> literule val argumentLiterule : conv -> int -> literule val allArgumentsLiterule : conv -> literule (* ------------------------------------------------------------------------- *) (* A rule takes one theorem and either deduces another or raises an Error *) (* exception. *) (* ------------------------------------------------------------------------- *) type rule = Thm.thm -> Thm.thm val allRule : rule val noRule : rule val thenRule : rule -> rule -> rule val orelseRule : rule -> rule -> rule val tryRule : rule -> rule val changedRule : rule -> rule val repeatRule : rule -> rule val firstRule : rule list -> rule val everyRule : rule list -> rule val literalRule : literule -> Literal.literal -> rule val rewrRule : equation -> Literal.literal -> Term.path -> rule val pathRule : conv -> Literal.literal -> Term.path -> rule val literalsRule : literule -> LiteralSet.set -> rule val allLiteralsRule : literule -> rule val convRule : conv -> rule (* All arguments of all literals *) (* ------------------------------------------------------------------------- *) (* *) (* --------- reflexivity *) (* x = x *) (* ------------------------------------------------------------------------- *) val reflexivityRule : Term.term -> Thm.thm val reflexivity : Thm.thm (* ------------------------------------------------------------------------- *) (* *) (* --------------------- symmetry *) (* ~(x = y) \/ y = x *) (* ------------------------------------------------------------------------- *) val symmetryRule : Term.term -> Term.term -> Thm.thm val symmetry : Thm.thm (* ------------------------------------------------------------------------- *) (* *) (* --------------------------------- transitivity *) (* ~(x = y) \/ ~(y = z) \/ x = z *) (* ------------------------------------------------------------------------- *) val transitivity : Thm.thm (* ------------------------------------------------------------------------- *) (* *) (* ---------------------------------------------- functionCongruence (f,n) *) (* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) (* f x0 ... x{n-1} = f y0 ... y{n-1} *) (* ------------------------------------------------------------------------- *) val functionCongruence : Term.function -> Thm.thm (* ------------------------------------------------------------------------- *) (* *) (* ---------------------------------------------- relationCongruence (R,n) *) (* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) (* ~R x0 ... x{n-1} \/ R y0 ... y{n-1} *) (* ------------------------------------------------------------------------- *) val relationCongruence : Atom.relation -> Thm.thm (* ------------------------------------------------------------------------- *) (* x = y \/ C *) (* -------------- symEq (x = y) *) (* y = x \/ C *) (* ------------------------------------------------------------------------- *) val symEq : Literal.literal -> rule (* ------------------------------------------------------------------------- *) (* ~(x = y) \/ C *) (* ----------------- symNeq ~(x = y) *) (* ~(y = x) \/ C *) (* ------------------------------------------------------------------------- *) val symNeq : Literal.literal -> rule (* ------------------------------------------------------------------------- *) (* sym (x = y) = symEq (x = y) /\ sym ~(x = y) = symNeq ~(x = y) *) (* ------------------------------------------------------------------------- *) val sym : Literal.literal -> rule (* ------------------------------------------------------------------------- *) (* ~(x = x) \/ C *) (* ----------------- removeIrrefl *) (* C *) (* *) (* where all irreflexive equalities. *) (* ------------------------------------------------------------------------- *) val removeIrrefl : rule (* ------------------------------------------------------------------------- *) (* x = y \/ y = x \/ C *) (* ----------------------- removeSym *) (* x = y \/ C *) (* *) (* where all duplicate copies of equalities and disequalities are removed. *) (* ------------------------------------------------------------------------- *) val removeSym : rule (* ------------------------------------------------------------------------- *) (* ~(v = t) \/ C *) (* ----------------- expandAbbrevs *) (* C[t/v] *) (* *) (* where t must not contain any occurrence of the variable v. *) (* ------------------------------------------------------------------------- *) val expandAbbrevs : rule (* ------------------------------------------------------------------------- *) (* simplify = isTautology + expandAbbrevs + removeSym *) (* ------------------------------------------------------------------------- *) val simplify : Thm.thm -> Thm.thm option (* ------------------------------------------------------------------------- *) (* C *) (* -------- freshVars *) (* C[s] *) (* *) (* where s is a renaming substitution chosen so that all of the variables in *) (* C are replaced by fresh variables. *) (* ------------------------------------------------------------------------- *) val freshVars : rule (* ------------------------------------------------------------------------- *) (* C *) (* ---------------------------- factor *) (* C_s_1, C_s_2, ..., C_s_n *) (* *) (* where each s_i is a substitution that factors C, meaning that the theorem *) (* *) (* C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C *) (* *) (* has fewer literals than C. *) (* *) (* Also, if s is any substitution that factors C, then one of the s_i will *) (* result in a theorem C_s_i that strictly subsumes the theorem C_s. *) (* ------------------------------------------------------------------------- *) val factor' : Thm.clause -> Subst.subst list val factor : Thm.thm -> Thm.thm list end [ Dauer der Verarbeitung: 0.128 Sekunden ] |