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.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-FOL-Fitting-2009-04-29.tar.gz Isabelle 2008: afp-FOL-Fitting-2008-06-10.tar.gz Isabelle 2007: afp-FOL-Fitting-2007-11-27.tar.gz