General models and extensionality
From MaRDI portal
Cited in
(25)- Unification under a mixed prefix
- A semantics for Prolog
- Embedding and automating conditional logics in classical higher-order logic
- Quantified multimodal logics in simple type theory
- Automating free logic in HOL, with an experimental application in category theory
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- Higher-order modal logics: automation and applications
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- A bit of history related to logic based on equality
- Analytic tableaux for higher-order logic with choice
- Identity, equality, nameability and completeness
- 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
- Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments
- 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
- Types, Tableaus and Gödel’s God in Isabelle/HOL
- Soundness of the Q0 proof system for higher-order logic
- Faithful Logic Embeddings in HOL — Deep and Shallow (Isabelle/HOL dataset)
- Abstract deduction and inferential models for type theory
This page was built for publication: General models and extensionality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5680123)
