(* 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