Leo III is a massively parallel higher-order theorem prover developed at the Freie Universität Berlin. In a nutshell, a reasoner is a tool a tool that can perform reasoning tasks for applications in a given domain. In the legal domain, a (non-exhaustive) list of reasoning tasks one would like to be able to perform is:

  • Compliance checking: is the current situation compliant with the norms?
  • Consistency checking: is such-and-such norm (part of the regulation) consistent with this other norm (part of another regulation)? Is such-and-such legal interpretation consistent with such-and-such legal interpretation?
  • Entailment checking: does such-and-such obligation or legal interpretation follow?

The University of Luxembourg and the Freie Universität Berlin are currently investigating ways to use Leo III for reasoning tasks in reified Input/Output logic.