FOL Fitting

swMATH ID: 28611
Software Authors: Stefan Berghofer; Andreas Halkjær From
Description: 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.
Homepage: https://www.isa-afp.org/entries/FOL-Fitting.html
Dependencies: Isabelle
Related Software: Archive Formal Proofs; Completeness theorem; Isabelle/HOL; HOL; Sledgehammer; Isabelle; Abstract Completeness; FOL_Harrison; Verified Prover; Superposition Calculus; GitHub; Isar; IsaFoL; SPASS; Epistemic Logic; SQEMA; Metamath; Isabelle/jEdit; Isabelle/Isar; Propositional Resolution
Referenced in: 6 Publications

Referencing Publications by Year