Email Gateway (Aug 22 2022 at 20:17): Email Gateway (Aug 22 2022 at 20:17):From: Tobias Nipkow <nipkow@in.tum.de>
A Sequent Calculus for First-Order Logic
Andreas Halkjær From
This work formalizes soundness and completeness of a one-sided sequent calculus
for first-order logic. The completeness is shown via a translation from a
complete semantic tableau calculus, the proof of which is based on the
First-Order Logic According to Fitting theory. The calculi and proof techniques
are taken from Ben-Ari's Mathematical Logic for Computer Science.
https://www.isa-afp.org/entries/FOL_Seq_Calc1.html
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC