diff options
Diffstat (limited to 'contrib/jprover/jall.mli')
| -rw-r--r-- | contrib/jprover/jall.mli | 339 |
1 files changed, 339 insertions, 0 deletions
diff --git a/contrib/jprover/jall.mli b/contrib/jprover/jall.mli new file mode 100644 index 00000000..1811fe59 --- /dev/null +++ b/contrib/jprover/jall.mli @@ -0,0 +1,339 @@ +(* JProver provides an efficient refiner for first-order classical + and first-order intuitionistic logic. It consists of two main parts: + a proof search procedure and a proof reconstruction procedure. + + + Proof Search + ============ + + The proof search process is based on a matrix-based (connection-based) + proof procedure, i.e.~a non-normalform extension procedure. + Besides the well-known quantifier substitution (Martelli Montanari), + a special string unifiation procedure is used in order to + efficiently compute intuitionistic rule non-permutabilities. + + + Proof Reconstruction + ==================== + + The proof reconstruction process converts machine-generated matrix proofs + into cut-free Gentzen-style sequent proofs. For classcal logic "C", + Gentzen's sequent calculus "LK" is used as target calculus. + For intuitionistic logic "J", either Gentzen's single-conclusioned sequent + calculus "LJ" or Fitting's multiply-conclusioned sequent calculus "LJmc" + can be used. All sequent claculi are implemented in a set-based formulation + in order to avoid structural rules. + + The proof reconstruction procedure combines three main procedures, depending + on the selected logics and sequent calculi. It consists of: + + 1) A uniform traversal algorithm for all logics and target sequent calculi. + This procedure converts classical (intuitionistic) matrix proofs + directly into cut-free "LK" ("LJmc" or "LJ") sequent proofs. + However, the direct construction of "LJ" proofs may fail in some cases + due to proof theoretical reasons. + + 2) A complete redundancy deletion algorithm, which integrates additional + knowledge from the proof search process into the reconstruction process. + This procedure is called by the traversal algorithms in order to avoid + search and deadlocks during proof reconstruciton. + + 3) A permutation-based proof transformation for converting "LJmc" proofs + into "LJ" proofs. + This procedure is called by-need, whenever the direct reconstruction + of "LJ" proofs from matrix proofs fails. + + + + + Literature: + ========== + + JProver system description was presented at CADE 2001: + @InProceedings{inp:Schmitt+01a, + author = "Stephan Schmitt and Lori Lorigo and Christoph Kreitz and + Alexey Nogin", + title = "{{\sf JProver}}: Integrating Connection-based Theorem + Proving into Interactive Proof Assistants", + booktitle = "International Joint Conference on Automated Reasoning", + year = "2001", + editor = "R. Gore and A. Leitsch and T. Nipkow", + volume = 2083, + series = LNAI, + pages = "421--426", + publisher = SPRINGER, + language = English, + where = OWN, + } + + The implementation of JProver is based on the following publications: + + + + Slides of PRL-seminar talks: + --------------------------- + + An Efficient Refiner for First-order Intuitionistic Logic + + http://www.cs.cornell.edu/Nuprl/PRLSeminar/PRLSeminar99_00/schmitt/feb28.html + + + An Efficient Refiner for First-order Intuitionistic Logic (Part II) + + http://www.cs.cornell.edu/Nuprl/PRLSeminar/PRLSeminar99_00/schmitt/may22.html + + + + Proof search: + ------------- + + +[1] + @InProceedings{inp:OttenKreitz96b, + author = "J.~Otten and C.~Kreitz", + title = "A uniform proof procedure for classical and + non-classical logics", + booktitle = "Proceedings of the 20$^{th}$ German Annual Conference on + Artificial Intelligence", + year = "1996", + editor = "G.~G{\"o}rz and S.~H{\"o}lldobler", + number = "1137", + series = LNAI, + pages = "307--319", + publisher = SPRINGER + } + + +[2] + @Article{ar:KreitzOtten99, + author = "C.~Kreitz and J.~Otten", + title = "Connection-based theorem proving in classical and + non-classical logics", + journal = "Journal for Universal Computer Science, + Special Issue on Integration of Deductive Systems", + year = "1999", + volume = "5", + number = "3", + pages = "88--112" + } + + + + + Special string unifiation procedure: + ------------------------------------ + + +[3] + @InProceedings{inp:OttenKreitz96a, + author = "J.~Otten and C.~Kreitz", + titl = "T-string-unification: unifying prefixes in + non-classical proof methods", + booktitle = "Proceedings of the 5$^{th}$ Workshop on Theorem Proving + with Analytic Tableaux and Related Methods", + year = 1996, + editor = "U.~Moscato", + number = "1071", + series = LNAI, + pages = "244--260", + publisher = SPRINGER, + month = "May " + } + + + + Proof reconstruction: Uniform traversal algorithm + ------------------------------------------------- + + +[4] + @InProceedings{inp:SchmittKreitz96a, + author = "S.~Schmitt and C.~Kreitz", + title = "Converting non-classical matrix proofs into + sequent-style systems", + booktitle = "Proceedings of the 13$^t{}^h$ Conference on + Automated Deduction", + editor = M.~A.~McRobbie and J.~K.~Slaney", + number = "1104", + series = LNAI, + pages = "418--432", + year = "1996", + publisher = SPRINGER, + month = "July/August" + } + + +[5] + @Article{ar:KreitzSchmitt00, + author = "C.~Kreitz and S.~Schmitt", + title = "A uniform procedure for converting matrix proofs + into sequent-style systems", + journal = "Journal of Information and Computation", + year = "2000", + note = "(to appear)" + } + + +[6] + @Book{bo:Schmitt00, + author = "S.~Schmitt", + title = "Proof reconstruction in classical and non-classical logics", + year = "2000", + publisher = "Infix", + series = "Dissertationen zur K{\"u}nstlichen Intelleigenz", + number = "(to appear)", + note = "(Ph.{D}.~{T}hesis, Technische Universit{\"a}t Darmstadt, + FG Intellektik, Germany, 1999)" + } + + The traversal algorithm is presented in the Chapters 2 and 3 of my thesis. + The thesis will be made available for the Department through Christoph Kreitz, + Upson 4159, kreitz@cs.cornell.edu + + + + + Proof reconstruction: Complete redundancy deletion + -------------------------------------------------- + + +[7] + @Book{bo:Schmitt00, + author = "S.~Schmitt", + title = "Proof reconstruction in classical and non-classical logics", + year = "2000", + publisher = "Infix", + series = "Dissertationen zur K{\"u}nstlichen Intelleigenz", + note = "(Ph.{D}.~{T}hesis, Technische Universit{\"a}t Darmstadt, + FG Intellektik, Germany, 1999)" + note = "(to appear)", + + } + + The integration of proof knowledge and complete redundancy deletion is presented + in Chapter 4 of my thesis. + + +[8] + @InProceedings{inp:Schmitt00, + author = "S.~Schmitt", + title = "A tableau-like representation framework for efficient + proof reconstruction", + booktitle = "Proceedings of the International Conference on Theorem Proving + with Analytic Tableaux and Related Methods", + year = "2000", + series = LNAI, + publisher = SPRINGER, + month = "June" + note = "(to appear)", + } + + + + + Proof Reconstruction: Permutation-based poof transformations "LJ" -> "LJmc" + --------------------------------------------------------------------------- + + +[9] + @InProceedings{inp:EglySchmitt98, + author = "U.~Egly and S.~Schmitt", + title = "Intuitionistic proof transformations and their + application to constructive program synthesis", + booktitle = "Proceedings of the 4$^{th}$ International Conference + on Artificial Intelligence and Symbolic Computation", + year = "1998", + editor = "J.~Calmet and J.~Plaza", + number = "1476", + series = LNAI, + pages = "132--144", + publisher = SPRINGER, + month = "September" + } + + +[10] + @Article{ar:EglySchmitt99, + author = "U.~Egly and S.~Schmitt", + title = "On intuitionistic proof transformations, their + complexity, and application to constructive program synthesis", + journal = "Fundamenta Informaticae, + Special Issue: Symbolic Computation and Artificial Intelligence", + year = "1999", + volume = "39", + number = "1--2", + pages = "59--83" + } +*) + +(*: open Refiner.Refiner +open Refiner.Refiner.Term +open Refiner.Refiner.TermType +open Refiner.Refiner.TermSubst + +open Jlogic_sig +:*) + +open Jterm +open Opname +open Jlogic + +val ruletable : rule -> string + +module JProver(JLogic: JLogicSig) : +sig + val test : term -> string -> string -> unit + + (* Procedure call: test conclusion logic calculus + + test is applied to a first-order formula. The output is some + formatted sequent proof for test / debugging purposes. + + The arguments for test are as follows: + + logic = "C"|"J" + i.e. first-order classical logic or first-order intuitionistic logic + + calculus = "LK"|"LJ"|"LJmc" + i.e. "LK" for classical logic "C", and either Gentzen's single conclusioned + calculus "LJ" or Fittings multiply-conclusioned calculus "LJmc" for + intuitionistic logic "J". + + term = first-order formula representing the proof goal. + *) + + + + val seqtest : term -> string -> string -> unit + + (* seqtest procedure is for debugging purposes only *) + + + val gen_prover : int option -> string -> string -> term list -> term list -> JLogic.inference + + (* Procedure call: gen_prover mult_limit logic calculus hypothesis conclusion + + The arguments for gen_prover are as follows: + + mult_limit - maximal multiplicity to try, None for unlimited + + logic = same as in test + + calculus = same as in test + + hypothesis = list of first-order terms forming the antecedent of the input sequent + + conclusion = list of first-order terms forming the succedent of the input sequent + This list should contain only one element if logic = "J" and calculus = "LJ". + *) + + + val prover : int option -> term list -> term -> JLogic.inference + + (* Procedure call: gen_prover mult_limit "J" "LJ" hyps [concl] + + prover provides the first-order refiner for NuPRL, using + a single concluisoned succedent [concl] in the sequent. + The result is a sequent proof in the single-conclusioned calculus "LJ". + *) +end |