A dyadic deontic logic in HOL

MaRDI QIDQ5224901zbMATHFDO

Authors Christoph Benzmüller, Ali Farjami, Xavier Parent

Publication date 24 July 2019

zbMATH Keywords

automated reasoningsemantic embeddingclassical higher-order logiclogic of CTD conditionals

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Recommendations

• Åqvist's dyadic deontic logic \(\mathbf{E}\) in HOL
• I/O logic in HOL
• Embedding and automating conditional logics in classical higher-order logic
• Interacting with Modal Logics in the Coq Proof Assistant
• Logical approaches to deontic reasoning: From basic questions to dynamic solutions

Cited in

(8)

• Extensional higher-order paramodulation in Leo-III
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• Norms and deontic logic
• Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments
• I/O logic in HOL
• Åqvist's dyadic deontic logic \(\mathbf{E}\) in HOL
• Maximality vs. optimality in dyadic deontic logic. Completeness results for systems in Hansson's tradition
• scientific article; zbMATH DE number 5863346 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nitpick
• Isabelle/HOL

This page was built for publication: A dyadic deontic logic in HOL

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