First-Order Logic According to Fitting

 

Title: First-Order Logic According to Fitting
Author: Stefan Berghofer
Submission date: 2007-08-02
Abstract: We present a formalization of parts of Melvin Fitting's book ``First-Order Logic and Automated Theorem Proving''. The formalization covers the syntax of first-order logic, its semantics, the model existence theorem, a natural deduction proof calculus together with a proof of correctness and completeness, as well as the Löwenheim-Skolem theorem.
BibTeX:
@article{FOL-Fitting-AFP,
  author  = {Stefan Berghofer},
  title   = {First-Order Logic According to Fitting},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2007,
  note    = {\url{http://isa-afp.org/entries/FOL-Fitting.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License