Basic first-order model theory in Mizar

MaRDI QIDQ3075243zbMATH OpenFDO

Authors Marco Caminati

Publication date 10 February 2011

Full work available at URL http://jfr.cib.unibo.it/article/view/1974

zbMATH Keywords

automated theorem provingclassical first-order model theoryMizar Mathematical Libraryproof checking

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Basic properties of first-order languages and structures (03C07)

Recommendations

• Preliminaries to classical first-order model theory
• scientific article; zbMATH DE number 1301853
• scientific article; zbMATH DE number 1507187
• Sequent calculus, derivability, provability. Gödel's completeness theorem
• The Gödel completeness theorem for uncountable languages

Cited in

(7)

• On rewriting rules in Mizar
• Formally verified tableau-based reasoners for a description logic
• The Gödel completeness theorem for uncountable languages
• Preliminaries to classical first-order model theory
• First order languages: further syntax and semantics
• Sequent calculus, derivability, provability. Gödel's completeness theorem
• scientific article; zbMATH DE number 1301853 (Why is no real title available?)

Describes a project that uses

Uses Software

• MML
• Mizar

This page was built for publication: Basic first-order model theory in Mizar

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075243)