Higher-order semantics and extensionality

DOI10.2178/jsl/1102022211zbMath1071.03024OpenAlexW2138366464WikidataQ57389428 ScholiaQ57389428MaRDI QIDQ5311767

Christoph Benzmüller, Michael Kohlhase, Chad Edward Brown

Publication date: 29 August 2005

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1102022211

zbMATH Keywords

consistencyextensionalitysemanticshigher-order modelsclassical higher-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order model theory (03C85)

Related Items

Cut-elimination for quantified conditional logic ⋮ Variants of Gödel's ontological proof in a natural deduction calculus ⋮ The higher-order prover \textsc{Leo}-II ⋮ Interacting with Modal Logics in the Coq Proof Assistant ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Quantified multimodal logics in simple type theory ⋮ Semantics of \textsc{OpenMath} and \textsc{MathML3} ⋮ Higher-Order Modal Logics: Automation and Applications ⋮ Analytic tableaux for higher-order logic with choice ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ Combining and automating classical and non-classical logics in classical higher-order logics ⋮ THF0 – The Core of the TPTP Language for Higher-Order Logic ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments ⋮ Kripke semantics for higher-order type theory applied to constraint logic programming languages ⋮ Analytic Tableaux for Higher-Order Logic with Choice ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ CERES in higher-order logic ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Agent-Based HOL Reasoning ⋮ THE DEVELOPMENT OF GÖDEL’S ONTOLOGICAL PROOF

Uses Software

• ETPS

Cites Work

• Automated deduction. A basis for applications. Vol. III: Applications
• An introduction to mathematical logic and type theory: To truth through proof.
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item