Isabelle FOL Fitting: First-Order Logic According to Fitting. 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.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Jensen, Alexander Birch; Larsen, John Bruntse; Schlichtkrull, Anders; Villadsen, Jørgen: Programming and verifying a declarative first-order prover in Isabelle/HOL (2018)
- Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
- Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
- Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2016)
- Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Unified classical logic completeness. A coinductive pearl (2014)