Higher-order semantics and extensionality
From MaRDI portal
Recommendations
Cites work
- An introduction to mathematical logic and type theory: To truth through proof.
- Automated deduction. A basis for applications. Vol. III: Applications
- Handbook of automated reasoning. In 2 vols
- scientific article; zbMATH DE number 837700 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
Cited in
(45)- Independence in higher-order subclassical logic
- Completeness and cut-elimination theorems for high-order classical logic. Constructive method
- Quantified multimodal logics in simple type theory
- Semantics of \textsc{OpenMath} and \textsc{MathML3}
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Automating free logic in HOL, with an experimental application in category theory
- Cut-elimination for quantified conditional logic
- Variants of Gödel's ontological proof in a natural deduction calculus
- Extensional higher-order paramodulation in Leo-III
- Agent-based HOL reasoning
- The higher-order prover \textsc{Leo}-II
- Higher-order modal logics: automation and applications
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Extended First-Order Logic
- Interacting with Modal Logics in the Coq Proof Assistant
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- scientific article; zbMATH DE number 1370937 (Why is no real title available?)
- scientific article; zbMATH DE number 1303338 (Why is no real title available?)
- scientific article; zbMATH DE number 1341621 (Why is no real title available?)
- Analytic tableaux for higher-order logic with choice
- scientific article; zbMATH DE number 1984522 (Why is no real title available?)
- scientific article; zbMATH DE number 1497799 (Why is no real title available?)
- scientific article; zbMATH DE number 1749187 (Why is no real title available?)
- scientific article; zbMATH DE number 6928628 (Why is no real title available?)
- THE DEVELOPMENT OF GÖDEL’S ONTOLOGICAL PROOF
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Theorem Proving in Higher Order Logics
- Analytic tableaux for higher-order logic with choice
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Solving modal logic problems by translation to higher-order logic
- Combining and automating classical and non-classical logics in classical higher-order logics
- Arithmetic is necessary
- Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments
- Tie-breaking semantics and structural totality
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- Faithful logic embeddings in HOL -- deep and shallow
- Notes on Gödel's and Scott's variants of the ontological argument
- Semantical investigations on non-classical logics with recovery operators: negation
- Solving quantified modal logic problems by translation to classical logics
- Nominal Henkin semantics: simply-typed lambda-calculus models in nominal sets
- 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
- Abstract deduction and inferential models for type theory
This page was built for publication: Higher-order semantics and extensionality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5311767)
