A Sequent Calculus for First-Order Logic (Q7361657)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry FOL_Seq_Calc1
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Sequent Calculus for First-Order Logic |
AFP entry FOL_Seq_Calc1 |
Statements
18 July 2019
0 references
Asta Halkjær From
0 references
Alexander Birch Jensen
0 references
Anders Schlichtkrull
0 references
Jørgen Villadsen
0 references
A Sequent Calculus for First-Order Logic (English)
0 references
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. Papers: ceur-ws.org/Vol-3002/paper7.pdf and doi.org/10.1093/logcom/exad013 .
0 references
