| products/sources/formale sprachen/Isabelle/Tools/Metis/src/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: NameArity.sig Sprache: VDM
|
rahmenlose Ansicht.sig DruckansichtAbap {Abap[116] [0] [0]}diese Dinge liegen außhalb unserer Verantwortung (* ========================================================================= *) (* THE RESOLUTION PROOF PROCEDURE *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Resolution = sig (* ------------------------------------------------------------------------- *) (* A type of resolution proof procedures. *) (* ------------------------------------------------------------------------- *) type parameters = {active : Active.parameters, waiting : Waiting.parameters} type resolution (* ------------------------------------------------------------------------- *) (* Basic operations. *) (* ------------------------------------------------------------------------- *) val default : parameters val new : parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} -> resolution val active : resolution -> Active.active val waiting : resolution -> Waiting.waiting val pp : resolution Print.pp (* ------------------------------------------------------------------------- *) (* The main proof loop. *) (* ------------------------------------------------------------------------- *) datatype decision = Contradiction of Thm.thm | Satisfiable of Thm.thm list datatype state = Decided of decision | Undecided of resolution val iterate : resolution -> state val loop : resolution -> decision end [ Verzeichnis aufwärts0.123unsichere Verbindung ] |