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 provingMizar Mathematical Libraryproof checkingclassical first-order model theory

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
• Publication:4503907
• Sequent calculus, derivability, provability. Gödel's completeness theorem
• The Gödel completeness theorem for uncountable languages

Cited in

(7)

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

Describes a project that uses

Uses Software

• Mizar
• MML

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)