Document Open Access Logo

Formalized Proof Systems for Propositional Logic

Authors Julius Michaelis , Tobias Nipkow

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2017.5.pdf
  • Filesize: 484 kB
  • 16 pages

Document Identifiers

Author Details

Julius Michaelis
  • Technische Universität München, Germany
Tobias Nipkow
  • Technische Universität München, Germany

Cite As Get BibTex

Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.TYPES.2017.5

Abstract

We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • formalization of logic
  • proof systems
  • sequent calculus
  • natural deduction
  • resolution

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Stefan Berghofer. First-Order Logic According to Fitting. Archive of Formal Proofs, 2007. , Formal proof development. URL: http://isa-afp.org/entries/FOL-Fitting.shtml.
  2. Jasmin C. Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. In N. Bjørner and V. Sofronie-Stokkermans, editors, Automated Deduction (CADE 2011), volume 6803 of LNCS, pages 116-130. Springer, 2011. Google Scholar
  3. Jasmin C. Blanchette et al. IsaFoL: Isabelle Formalization of Logic. URL: https://bitbucket.org/isafol/isafol.
  4. Jasmin C. Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Accepted for publication in J. of Automated Reasoning, 2018. Google Scholar
  5. Jasmin C. Blanchette, Mathias Fleury, and Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart, and incrementality. In N. Olivetti and A. Tiwari, editors, Automated Reasoning (IJCAR 2016), volume 9706 of LNCS, pages 25-44. Springer, 2016. Google Scholar
  6. Jasmin C. Blanchette, Andrei Popescu, and Dmitriy Traytel. Unified Classical Logic Completeness. In S. Demri, D. Kapur, and C. Weidenbach, editors, Automated Reasoning (IJCAR 2014), volume 8562 of LNCS, pages 46-60. Springer, 2014. Google Scholar
  7. Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers - an overview. Mathematical Structures in Computer Science, 26(1):38-88, 2016. URL: http://dx.doi.org/10.1017/S0960129514000115.
  8. Patrick Braselmann and Peter Koepke. Gödel’s Completeness Theorem. Formalized Mathematics, 13(1):49-53, 2005. URL: http://fm.mizar.org/2005-13/pdf13-1/goedelcp.pdf.
  9. Peter Chapman, James McKinna, and Christian Urban. Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. In Proc. AISC/Calculemus/MKM Conference, pages 38-52. Springer, 2008. Google Scholar
  10. Kaustuv Chaudhuri, Leonardo Lima, and Giselle Reis. Formalized Meta-Theory of Sequent Calculi for Substructural Logics. In Workshop on Logical and Semantic Frameworks, with Applications (LSFA-11), 2016. Google Scholar
  11. Christian Doczkal and Gert Smolka. Completeness and Decidability Results for CTL in Constructive Type Theory. Automated Reasoning, 56(3):343-365, 2016. Google Scholar
  12. Herbert Enderton. A Mathematical Introduction to Logic. Academic Press, 1972. Google Scholar
  13. Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1990. Google Scholar
  14. Andrew Gacek. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. PhD thesis, University of Minnesota, 2009. Google Scholar
  15. Jean H Gallier. Logic for computer science: foundations of automatic theorem proving. Harper &Row, 1986. Google Scholar
  16. John Harrison. Formalizing Basic First Order Model Theory. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics (TPHOLs '98), volume 1497 of LNCS, pages 153-170. Springer, 1998. Google Scholar
  17. John Harrison. Towards self-verification of HOL Light. In U. Furbach and N. Shankar, editors, Automated Reasoning (IJCAR 2006), volume 4130 of LNCS, pages 177-191. Springer, 2006. Google Scholar
  18. John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. Google Scholar
  19. David Hilbert. Die Grundlagen der Mathematik. Vieweg+Teubner Verlag, Wiesbaden, 1928. URL: http://dx.doi.org/10.1007/978-3-663-16102-8_1.
  20. Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, 2004. Google Scholar
  21. Danko Illik. Constructive Completeness Proofs and Delimited Control. PhD thesis, École Polytechnique, 2010. Google Scholar
  22. Alexander Krauss. Recursive Definitions of Monadic Functions. In Ekaterina Komendantskaya, Ana Bove, and Milad Niqui, editors, Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, volume 5 of EPiC Series, pages 1-13. EasyChair, 2012. URL: http://www.easychair.org/publications/?page=2065850452.
  23. Ramana Kumar, Rob Arthan, Magnus Myreen, and Scott Owens. Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. Autom. Reasoning, 56(3):221-259, 2016. Google Scholar
  24. Stephane Lescuyer. Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. PhD thesis, Université Paris Sud - Paris XI, 2011. Google Scholar
  25. Filip Marić. Formalization and implementation of modern SAT solvers. Automated Reasoning, 43(1):81-119, 2009. Google Scholar
  26. Julius Michaelis and Tobias Nipkow. Propositional Proof Systems. Archive of Formal Proofs, June 2017. , Formal proof development. URL: http://isa-afp.org/entries/Propositional_Proof_Systems.html.
  27. Tobias Nipkow. Linear Quantifier Elimination. Automated Reasoning, 45:189-212, 2010. Google Scholar
  28. Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
  29. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  30. Duckki Oe, Aaron Stump, Corey Oliver, and Kevin Clancy. versat: A verified modern SAT solver. In V. Kuncak and A. Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI 2012), volume 7148 of LNCS, pages 24-38. Springer, 2012. Google Scholar
  31. Lawrence C. Paulson. A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle. Autom. Reasoning, 55(1):1-37, 2015. Google Scholar
  32. Frank Pfenning. Elf: A Language for Logic Definition and Verified Metaprogramming. In Logic in Computer Science (LICS 1989), pages 313-322. IEEE Computer Society Press, 1989. Google Scholar
  33. Frank Pfenning. Structural Cut Elimination: I. Intuitionistic and Classical Logic. Inf. Comput., 157(1-2):84-141, 2000. Google Scholar
  34. Frank Pfenning and Carsten Schürmann. System description: Twelf - A Meta-Logical Framework for Deductive Systems. In H. Ganzinger, editor, Automated Deduction - CADE-16, volume 1632 of LNCS, pages 202-206. Springer, 1999. Google Scholar
  35. Brigitte Pientka and Andrew Cave. Inductive Beluga: Programming Proofs. In A. Felty and A. Middeldorp, editors, Automated Deduction (CADE-25), volume 9195 of LNCS, pages 272-281. Springer, 2015. Google Scholar
  36. Tom Ridge and James Margetson. A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. In J. Hurd and T. Melham, editors, Theorem Proving in Higher Order Logic (TPHOLs 2005), volume 3603 of LNCS, pages 294-309. Springer, 2005. Google Scholar
  37. Anders Schlichtkrull. Formalization of the Resolution Calculus for First-Order Logic. In J. Blanchette and S. Merz, editors, Interactive Theorem Proving (ITP 2016), volume 9807 of LNCS, pages 341-357. Springer, 2016. Google Scholar
  38. Anders Schlichtkrull. Formalization of the Resolution Calculus for First-Order Logic. J. of Automated Reasoning, January 2018. URL: http://dx.doi.org/10.1007/s10817-017-9447-z.
  39. Julian J. Schlöder and Peter Koepke. The Gödel completeness theorem for uncountable languages. Formalized Mathematics, 20(3):199-203, 2012. URL: http://dx.doi.org/10.2478/v10037-012-0023-z.
  40. Uwe Schöning. Logic for Computer Scientists. Birkhäuser, 1989. Google Scholar
  41. Kurt Schütte. Schlußweisen-Kalküle der Prädikatenlogik. Mathematische Annalen, 122(1):47-65, 1950. URL: http://dx.doi.org/10.1007/BF01342950.
  42. Natarajan Shankar. Metamathematics, Machines, and Gödel’s Proof. Cambridge University Press, 1994. Google Scholar
  43. Natarajan Shankar and Marc Vaucher. The Mechanical Verification of a DPLL-Based Satisfiability Solver. Electr. Notes Theor. Comput. Sci., 269:3-17, 2011. Google Scholar
  44. Raymond M Smullyan. A unifying principal in quantification theory. Proceedings of the National Academy of Sciences, 49(6):828-832, 1963. Google Scholar
  45. Raymond M. Smullyan. First-Order Logic. Springer, 1968. Google Scholar
  46. Christian Sternagel, René Thiemann, et al. IsaFoR/CeTA: An Isabelle/HOL formalization of rewriting for certified termination analysis. URL: http://cl-informatik.uibk.ac.at/software/ceta/.
  47. René Thiemann and Christian Sternagel. Certification of Termination Proofs Using CeTA. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Theorem Proving in Higher Order Logic (TPHOLs 2009), volume 5674 of LNCS, pages 452-468. Springer, 2009. Google Scholar
  48. A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2nd edition, 2000. Google Scholar
  49. Christian Urban and Bozhi Zhu. Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. In A. Voronkov, editor, Rewriting Techniques and Applications (RTA 2008), volume 5117 of LNCS, pages 409-424. Springer, 2008. Google Scholar
  50. Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad, and S. Arun-Kumar. Reflecting BDDs in Coq. In He Jifeng and Masahiko Sato, editors, ASIAN 2000: 6th Asian Computing Science Conference, volume 1961 of LNCS, pages 162-181. Springer, 2000. Google Scholar
  51. Bruno Woltzenlogel Paleo, editor. Towards an Encyclopaedia of Proof Systems. College Publications, London, UK, 1 edition, January 2017. URL: https://github.com/ProofSystem/Encyclopedia/blob/master/main.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact