Formalizing basic first order model theory

DOI10.1007/BFB0055135MaRDI QIDQ4247076zbMATH OpenFDO

Authors John R. Harrison

Publication date 15 February 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0055135

zbMATH Keywords

canonical term modelsCompactnessHOL datatypeHOL Light theorem proverLöwenheim-SkolemsatisfiabilitysemanticsSkolemizationsyntaxUniformityunsorted first-order logicvalidity

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 638363
• Preliminaries to classical first-order model theory
• Basic first-order model theory in Mizar
• Beyond first order model theory
• scientific article; zbMATH DE number 957948
• scientific article; zbMATH DE number 1418078
• Automatic models of first order theories
• scientific article; zbMATH DE number 139760
• On First-Order Model-Based Reasoning
• First-order logic theorem proving and model building via approximation and instantiation

Cited in

(22)

• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formalization of the resolution calculus for first-order logic
• Extending to a model structure is not a first-order property
• Mechanised modal model theory
• First-order abduction as enumeration of stable models
• Formally verified tableau-based reasoners for a description logic
• Soundness and completeness proofs by coinductive methods
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formalization of the Resolution Calculus for First-Order Logic
• On First-Order Model-Based Reasoning
• Basic first-order model theory in Mizar
• A verified runtime for a verified theorem prover
• Bases for first-order theories and subtheories
• Automatic models of first order theories
• scientific article; zbMATH DE number 1418078 (Why is no real title available?)
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• Hall's theorem for enumerable families of finite sets
• A modular formalization of superposition in Isabelle/HOL
• Abstract, compositional consistency: Isabelle/HOL locales for completeness à la fitting
• Formalizing splitting in Isabelle/HOL
• Compactness Theorem for First-Order Logic
• First order theories for partial models

Describes a project that uses

Uses Software

• HOL Light

This page was built for publication: Formalizing basic first order model theory

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