LogiKEy

LogiKEy enables formal ethical and legal reasoning by providing formal encodings of multiple deontic logics, their combinations, and analyses of deontic paradoxes within the higher-order proof assistant Isabelle/HOL.

Key Features:

• Formal encodings: Includes formal encodings of a range of deontic logics and normative theories provided as Isabelle/HOL theory files for rigorous logical analysis.
• Multiple deontic logics and combinations: Supports the use and combination of multiple deontic logics and addresses deontic paradoxes.
• Higher-order reasoning: Operates within the higher-order proof assistant Isabelle/HOL to enable mechanized proof and verification.
• Dataset repository: Serves as a repository of formalized normative theories and related artefacts for experimentation and reuse.
• LogiKEy methodology support: Implements the LogiKEy methodology to facilitate systematic experimentation with normative theories across contexts.

Scientific Applications:

• Research consolidation: Consolidates related research contributions and formalizations to provide a foundation for comparative studies of normative theories.
• Educational use: Supports teaching and hands-on exploration of complex logic formalisms and deontic reasoning in academic settings.

Methodology:

The LogiKEy methodology facilitates flexible, expressive experimentation with various normative theories and their formalization as Isabelle/HOL theory files.