IsaFoL: Isabelle Formalization of Logic

This repository contains various Isabelle formalizations of logical calculi and related topics.

The goal is to develop lemma libraries and methodology for formalizing modern research in automated reasoning. Our initial focus is on well-established ground and first-order calculi, such as DPLL, CDCL, and resolution. One of our inspirations is the IsaFoR/CeTA project (Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions) at Universität Innsbruck.

Entries

A Comprehensive Saturation Framework

• Latest version (compatible with latest Isabelle repository): AFP entry 1; AFP entry 2
• Recent version (compatible with latest Isabelle release): AFP entry 1; AFP entry 2

A Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

A Variant of the Superposition Calculus

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Abstract Completeness

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Abstract Soundness

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Epistemic Logic

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

First-Order Logic According to Berghofer (ongoing)

• Latest version (compatible with latest Isabelle release): IsaFoL entry

First-Order Logic According to Harrison

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry
• Variants (compatible with latest Isabelle release): IsaFoL entry

First-Order Logic According to Monk (ongoing)

• Latest version (compatible with latest Isabelle release): IsaFoL entry

GRAT Checker

• Latest version (compatible with Isabelle2016-1): IsaFoL entry

Hybrid Logic

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry
• Variants (compatible with latest Isabelle release): IsaFoL entry

Lambda-Free Higher-Order Embedding Path Order

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Lambda-Free Higher-Order Knuth-Bendix Orders

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Lambda-Free Higher-Order Recursive Path Orders

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Ordered Resolution Prover According to Bachmair and Ganzinger

• Latest version (compatible with Isabelle2017): IsaFoL entry, documentation

Paraconsistency

• Latest version (compatible with latest Isabelle release): IsaFoL entry
• Recent version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

PAC Checker

The initial formalisation of PAC was moved to the AFP:

• Latest version (compatible with latest Isabelle release): AFP entry
• AFP entry (compatible with latest Isabelle release): AFP entry

But we continued working on it in IsaFoL entry

Proof Systems for Propositional Logic

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry
• Isabelle2016-1-compatible version: IsaFoL entry, documentation

Propositional Resolution and Prime Implicates Generation

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Sequent Calculus

• Latest version (compatible with latest Isabelle release): IsaFoL entry

Simple Prover

• Latest version (compatible with latest Isabelle release): IsaFoL entry

Sound and Complete Sort Encodings for First-Order Logic

• Latest version (compatible with latest Isabelle repository): AFP entry
• Recent version (compatible with latest Isabelle release): AFP entry

Standard Superposition (ongoing)

• Latest version (compatible with latest Isabelle release): IsaFoL entry

Unordered Resolution

• Latest version (compatible with latest Isabelle release): AFP entry, IsaFoL entry, documentation
• Recent version (compatible with latest Isabelle repository): AFP entry
• Isabelle2016-compatible version described at ITP 2016: IsaFoL entry, documentation

Weidenbach's Book (ongoing)

• The relevant parts of Weidenbach's book can be found online
• Latest version (compatible with Isabelle version 2017): IsaFoL entry, documentation
• Isabelle2016-compatible version described at IJCAR 2016: IsaFoL entry, documentation

Authors

• Heiko Becker
• Alexander Bentkamp
• Jasmin Christian Blanchette
• Mathias Fleury
• Asta Halkjær From (Andreas)
• Alexander Birch Jensen
• Peter Lammich
• John Bruntse Larsen
• Julius Michaelis
• Tobias Nipkow
• Nicolas Peltier
• Andrei Popescu
• Simon Robillard
• Anders Schlichtkrull
• Sophie Tourret
• Dmitriy Traytel
• Jørgen Villadsen
• Petar Vukmirović

Additional Collaborators

• Maximilian Kirchmeier
• Christian Sternagel
• Uwe Waldmann
• Daniel Wand
• Christoph Weidenbach

Publications

• The Proof Checkers Pacheck and Past`equefor the Practical Algebraic Calculus. D. Kaufmann, M. Fleury, and A Biere. Formal Methods in Computer-Aided Design 2020 (FMCAD-20).

• A Verified SAT Solver Framework including Optimization and Partial Valuations. M. Fleury and C. Weidenbach. Accepted at 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23).

• A Comprehensive Framework for Saturation Theorem Proving. U. Waldmann, S. Tourret, S. Robillard, and J. Blanchette Accepted at 10th International Joint Conference on Automated Reasoning (IJCAR 2020).

• Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. A. Schlichtkrull, J. Blanchette, D. Traytel, and U. Waldmann. Acccepted in Journal of Automated Reasoning.

• Formalization of Logical Calculi in Isabelle/HOL M. Fleury. Ph.D. thesis, Universität des Saarlandes, 2020.

• Optimizing a Verified SAT Solver. M. Fleury. In Badger, J., Rozier, K.Y. (eds.) 11th NASA Formal Methods Symposium (NFM 2019), LNCS, Springer, 2019.

• A Verified Prover Based on Ordered Resolution. A. Schlichtkrull, J. C. Blanchette, and D. Traytel. In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), ACM, 2019.

• Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk) J. C. Blanchette. In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), ACM, 2019.

• Formalization of Logic in the Isabelle Proof Assistant A. Schlichtkrull. Ph.D. thesis, Technical University of Denmark, 2018.

• Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. A. Schlichtkrull, J. C. Blanchette, D. Traytel, and U. Waldmann. In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018), LNCS 10395, pp. 89–107, Springer, 2018.

• A Verified SAT Solver with Watched Literals using Imperative HOL (Extended Abstract) M. Fleury, J. C. Blanchette, and P. Lammich. Isabelle Workshop 2018.

• Formalization of the Resolution Calculus for First-Order Logic A. Schlichtkrull. Journal of Automated Reasoning 61(1-4):455-484, 2018.

• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. C. Blanchette, M. Fleury, P. Lammich, and C. Weidenbach. Journal of Automated Reasoning 61(1-4):333-365, 2018.

• Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant. J. Villadsen and A. Schlichtkrull. LNCS Transactions on Large-Scale Data- and Knowledge-Centered Systems 34:92-122, 2017.

• A Verified SAT Solver with Watched Literals using Imperative HOL. M. Fleury, J. C. Blanchette, and P. Lammich. In Andronick, J., Felty, A. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), ACM, 2018.

• The GRAT Tool Chain: Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. P. Lammich. In Gaspers, S., Walsh, T. (eds.) 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017), LNCS 10491, pp. 457–463, Springer, 2017.

• Efficient Verified (UN)SAT Certificate Checking. P. Lammich. In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE-26), LNCS 10395, pp. 237–254, Springer, 2017.

• Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. J. C. Blanchette, M. Fleury, and D. Traytel. In Miller, D. (ed.) 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), LIPIcs 84, pages 11:1–11:18, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2017.

• A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms. H. Becker, J. C. Blanchette, U. Waldmann, and D. Wand. In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE-26), LNCS 10395, pp. 432–453, Springer, 2017.

• A Lambda-Free Higher-Order Recursive Path Order. J. C. Blanchette, U. Waldmann, and D. Wand. In Esparza, J., Murawski, A. S. (eds.) 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), LNCS 10203, pp. 461–479, Springer, 2017.

• Soundness and Completeness Proofs by Coinductive Methods. J. C. Blanchette, A. Popescu, and D. Traytel. Journal of Automated Reasoning 58(1):149-179, 2017.

• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. C. Blanchette, M. Fleury, and C. Weidenbach. In Sierra, C. (ed.) 26th International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 4786–4790, ijcai.org, 2017.

• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract) J. C. Blanchette, M. Fleury, P. Lammich, and C. Weidenbach. Isabelle Workshop 2016.

• Formalization of the Resolution Calculus for First-Order Logic. A. Schlichtkrull. In Blanchette, J. C., Merz, S. (eds.) 7th International Conference on Interactive Theorem Proving (ITP 2016), LNCS 9807, pp. 341-357, Springer, 2016.

• Development and Verification of a Proof Assistant. A. B. Jensen. M.Sc. thesis, Technical University of Denmark, 2016.

• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. C. Blanchette, M. Fleury, and C. Weidenbach. In Olivetti, N., Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016), LNCS 9706, pp. 25-44, Springer, 2016.

• Meta-Logical Reasoning in Higher-Order Logic. J. Villadsen, A. Schlichtkrull, and A. V. Hess. Poster session presented at 29th Annual International Symposia Devoted to Logic (LOGICA 2015), 2015.

• Formalization of Resolution Calculus in Isabelle. A. Schlichtkrull. M.Sc. thesis, Technical University of Denmark, 2015.

• Formalisation of Ground Inference Systems in a Proof Assistant. M. Fleury. M.Sc. thesis, École normale supérieure Rennes, 2015.

• Unified Classical Logic Completeness: A Coinductive Pearl. J. C. Blanchette, A. Popescu, and D. Traytel. In Demri, S., Kapur, D., Weidenbach, C. (eds) 7th International Joint Conference on Automated Reasoning (IJCAR 2014), LNCS 8562, pp. 46-60, Springer, 2014.

• Mechanizing the Metatheory of Sledgehammer. J. C. Blanchette and A. Popescu. In Fontaine, P., Ringeissen, C., Schmidt, R. A. (eds.) 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), LNCS 8152, pp. 245-260, Springer, 2013.