Completeness theorem

swMATH ID: 28562
Software Authors: James Margetson; Tom Ridge
Description: Completeness theorem: The completeness of first-order logic is proved, following the first five pages of Wainer and Wallen’s chapter of the book Proof Theory by Aczel et al., CUP, 1992. Their presentation of formulas allows the proofs to use symmetry arguments. Margetson formalized this theorem by early 2000. The Isar conversion is thanks to Tom Ridge.
Homepage: https://www.isa-afp.org/entries/Completeness.html
Dependencies: Isabelle
Related Software: Archive Formal Proofs; Isabelle/HOL; FOL Fitting; HOL; Sledgehammer; Isabelle; Isar; Abstract Completeness; IsaFoL; FOL_Harrison; Verified Prover; Superposition Calculus; GitHub; Jitawa; Milawa; LCF; SPASS; ML; HOL Light; Metamath
Referenced in: 8 Publications

Referencing Publications by Year