A Sequent Calculus for First-Order Logic

Asta Halkjær From with contributions from Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen

18 July 2019


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.
BSD License

Depends On