Isabelle/HOL is an interactive theorem prover (proof assistant) for classical higher-order logic with choice. It has originally been developed by Lawrence Paulson (University of Cambridge) in the 1980s and further developed by many others. Isabelle/HOL can be used to formalize complex theories and allows formal reasoning about them, e.g. for software verification. In the context of normative and legal reasoning, we use Isabelle/HOL for:

  • Formalizing non-classical logics that are used for knowledge representation and reasoning in this domain,
  • Proving correctness of semantical embeddings to higher-order logic (see also Leo-III), and
  • fast prototyping of reasoning tools for computer-assisted assessment of normative and legal scenarios

 

Main contributors: Christoph Benzmüller, Alexander Steen