Email Gateway (Mar 29 2022 at 12:20): Email Gateway (Mar 29 2022 at 12:20):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new AFP entry.
A Naive Prover for First-Order Logic
by Asta Halkjær From
The AFP entry Abstract Completeness by Blanchette, Popescu and Traytel
formalizes the core of Beth/Hintikka-style completeness proofs for first-order
logic and can be used to formalize executable sequent calculus provers. In the
Journal of Automated Reasoning, the authors instantiate the framework with a
sequent calculus for first-order logic and prove its completeness. Their use of
an infinite set of proof rules indexed by formulas yields very direct arguments.
A fair stream of these rules controls the prover, making its definition
remarkably simple. The AFP entry, however, only contains a toy example for
propositional logic. The AFP entry A Sequent Calculus Prover for First-Order
Logic with Functions by From and Jacobsen also uses the framework, but uses a
finite set of generic rules resulting in a more sophisticated prover with more
complicated proofs.
This entry contains an executable sequent calculus prover for first-order logic
with functions in the style presented by Blanchette et al. The prover can be
exported to Haskell and this entry includes formalized proofs of its soundness
and completeness. The proofs are simpler than those for the prover by From and
Jacobsen but the performance of the prover is significantly worse.
The included theory Fair-Stream first proves that the sequence of natural
numbers 0, 0, 1, 0, 1, 2, etc. is fair. It then proves that mapping any
surjective function across the sequence preserves fairness. This method of
obtaining a fair stream of rules is similar to the one given by Blanchette et
al. The concrete functions from natural numbers to terms, formulas and rules are
defined using the Nat-Bijection theory in the HOL-Library.
https://www.isa-afp.org/entries/FOL_Seq_Calc3.html
Enjoy,
René
Last updated: Jul 15 2022 at 23:21 UTC