Basic first-order model theory in Mizar

zbMATH Open1211.03024MaRDI QIDQ3075243FDOQ3075243

Authors: Marco Caminati 

Publication date: 10 February 2011

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

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

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)

Cited In (7)

• First order languages: further syntax and semantics
• Preliminaries to classical first-order model theory
• The Gödel completeness theorem for uncountable languages
• Sequent calculus, derivability, provability. Gödel's completeness theorem
• On rewriting rules in Mizar
• Formally verified tableau-based reasoners for a description logic
• Title not available (Why is that?)

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)