[isabelle] New AFP entry: A Sequent Calculus for First-Order Logic



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!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.