IsaFoL: Isabelle Formalization of Logic

This repository contains various ongoing Isabelle formalizations of logical calculi.

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 Termination Analysis) at Universität Innsbruck.

News: The paper A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality has received the Best Paper Award at IJCAR 2016.

Entries

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

Bachmair & Ganzinger (ongoing)

• Latest version (compatible with recent Isabelle repository): IsaFoL entry, documentation
• Isabelle2016-compatible version: IsaFoL entry, documentation

First-Order Logic According to Berghofer (ongoing)

• Latest version (compatible with Isabelle2016-1): 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 Isabelle2016-1): IsaFoL entry

GRAT Checker

• Latest version (compatible with Isabelle2016-1): IsaFoL 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

Paraconsistency

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

Proof Systems for Propositional Logic

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

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

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)

• Latest version (compatible with recent Isabelle repository): IsaFoL entry, documentation
• Isabelle2016-compatible version described at IJCAR 2016: IsaFoL entry, documentation

Authors

• Heiko Becker
• Jasmin Christian Blanchette
• Mathias Fleury
• Andreas Halkjær From
• Alexander Birch Jensen
• Maximilian Kirchmeier
• Peter Lammich
• John Bruntse Larsen
• Julius Michaelis
• Tobias Nipkow
• Andrei Popescu
• Anders Schlichtkrull
• Sophie Tourret
• Dmitriy Traytel
• Jørgen Villadsen

Additional Collaborators

• Uwe Waldmann
• Daniel Wand
• Christoph Weidenbach

Publications

• Efficient verified (UN)SAT certificate checking. P. Lammich. Accepted at 26th International Conference on Automated Deduction (CADE-26).

• A transfinite Knuth–Bendix order for lambda-free higher-order terms. H. Becker, J. C. Blanchette, U. Waldmann, and D. Wand. Accepted at 26th International Conference on Automated Deduction (CADE-26).

• 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.

• 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.