Completeness theorem

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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 8 articles )

Showing results 1 to 8 of 8.
Sorted by year (citations)

  1. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  2. Jensen, Alexander Birch; Larsen, John Bruntse; Schlichtkrull, Anders; Villadsen, Jørgen: Programming and verifying a declarative first-order prover in Isabelle/HOL (2018)
  3. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  4. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  5. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
  6. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2016)
  7. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Unified classical logic completeness. A coinductive pearl (2014)
  8. Hidalgo-Doblado, M. J.; Alonso-Jiménez, J. A.; Borrego-Díaz, J.; Martín-Mateos, F. J.; Ruiz-Reina, J. L.: Formally verified tableau-based reasoners for a description logic (2014)