Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments

DOI10.1007/978-3-030-70084-3_14MaRDI QIDQ6618558zbMATH OpenFDO

Authors Christoph Benzmüller, Ali Farjami, Xavier Parent

Publication date 14 October 2024

Full work available at URL https://doi.org/10.1007/978-3-030-70084-3_14

zbMATH Keywords

classical higher-order logicdyadic deontic logicfaithfulnesssemantic embedding

Mathematics Subject Classification ID

Higher-order logic (03B16) Modal logic (including the logic of norms) (03B45) Other applications of logic (03B80)

Recommendations

• A dyadic deontic logic in HOL
• Åqvist's dyadic deontic logic \(\mathbf{E}\) in HOL
• I/O logic in HOL
• Embedding and automating conditional logics in classical higher-order logic
• Automating free logic in Isabelle/HOL

Cites work

• A formulation of the simple theory of types.
• A set of postulates for the foundation of logic. I, II.
• An Unsolvable Problem of Elementary Number Theory
• Completeness and decidability results for a logic of contrary-to-duty conditionals
• Completeness in the theory of types
• Cut-elimination for quantified conditional logic
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• Extending Sledgehammer with SMT solvers
• General models and extensionality
• General models, descriptions, and choice in type theory
• Handbook of philosophical logic. Vol. 8
• Higher-order semantics and extensionality
• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 7015113 (Why is no real title available?)
• Intensional models for the theory of types
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanised assessment of complex natural-language arguments using expressive logic combinations
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Quantified multimodal logics in simple type theory
• Resolution in type theory

This page was built for publication: Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments

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