Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: A Sequent Calculus for First-Or...


view this post on Zulip 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: Mar 28 2024 at 12:29 UTC