| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
A Sequent Calculus for First-Order Logic
| Title: | A Sequent Calculus for First-Order Logic |
| Author: | Asta Halkjær From |
| Contributors: | Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen |
| Submission date: | 2019-07-18 |
| 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. |
| BibTeX: |
@article{FOL_Seq_Calc1-AFP,
author = {Asta Halkjær From},
title = {A Sequent Calculus for First-Order Logic},
journal = {Archive of Formal Proofs},
month = jul,
year = 2019,
note = {\url{http://isa-afp.org/entries/FOL_Seq_Calc1.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | FOL-Fitting |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |