Monadic Second-Order Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Isabelle/HOL dataset)
by Christoph Benzmüller and Daniel Kirchner
by Christoph Benzmüller and Daniel Kirchner
Logic/General logic/Mechanization of proofs
Subject Classification
AMS: Mathematical logic and foundations / General logic / Mechanization of proofs and logical operations
2026
by Christoph Benzmüller and Daniel Kirchner
Mechanized Metasemantics of Modal Necessity: Valuation Factorization and Modal Non-Collapse
by Kim, Yong-Dock
Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL
by Kim, Yong-Dock
2025
A Modular Splitting Framework for Saturation Theorem Proving
by Ghilain Bergeron, Florent Krasnopol and Sophie Tourret
2024
2023
A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic
by Martin Desharnais-Schäfer
2022
A Sequent Calculus Prover for First-Order Logic with Functions
by Asta Halkjær From and Frederik Krogsdal Jacobsen
2020
Extensions to the Comprehensive Framework for Saturation Theorem Proving
by Jasmin Christian Blanchette and Sophie Tourret
2019
2018
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann
2017
First-Order Logic According to Harrison
by Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen
2016
2014
2013
Sound and Complete Sort Encodings for First-Order Logic
by Jasmin Christian Blanchette and Andrei Popescu
2004
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
by Tom Ridge