Higher-order semantics and extensionality

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

Michael Kohlhase, Christoph Benzmüller, 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

consistency; extensionality; semantics; higher-order models; classical higher-order logic

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03C85: Second- and higher-order model theory

Related Items

Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Analytic Tableaux for Higher-Order Logic with Choice, Analytic tableaux for higher-order logic with choice, Combining and automating classical and non-classical logics in classical higher-order logics, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, CERES in higher-order logic, TPS: A hybrid automatic-interactive system for developing proofs, Quantified multimodal logics in simple type theory, Semantics of \textsc{OpenMath} and \textsc{MathML3}, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners), THF0 – The Core of the TPTP Language for Higher-Order Logic

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