Abstract
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.
| Original language | English |
|---|---|
| Book series | Archive of Formal Proofs |
| Volume | 2021 |
| Number of pages | 24 |
| ISSN | 2150-914X |
| Publication status | Published - 2021 |