Von Objekt- und Meta-Ebenen: Analyse der Softwareanforderungen computergestützter juristischer Entscheidungen

in Recht DIGITAL – 25 Jahre IRIS, Proceedings of the International Legal Informatics Symposium (IRIS 2022) (in press)

Die Interpretation und Anwendung von Gesetzestexten auf einem konkreten Lebenssachverhalt erfordert von menschlichen Experten ein hohes Maß an Wissen, Erfahrung und die Fähigkeit zahlreiche kontextuelle ... [more ▼]

Die Interpretation und Anwendung von Gesetzestexten auf einem konkreten Lebenssachverhalt erfordert von menschlichen Experten ein hohes Maß an Wissen, Erfahrung und die Fähigkeit zahlreiche kontextuelle Überlegungen anzustellen. Die Formalisierung und Automatisierung solch eines Prozesses in einem computergestützten Verfahren muss dies entsprechend reflektieren. Ausgehend von einer Fallstudie werden in dieser Arbeit erforderliche juridische Schritte der Rechtsanwendung identifiziert und verschiedenen Objekt- und Meta-Ebenen zugeordnet. Diese Zuordnung erlaubt eine abstrakte Analyse von Softwareanforderungen, die juristische Assistenzsysteme erfüllen müssen, um bei juristischen Fallentscheidungen unterstützen zu können. [less ▲]

A Formalisation of Abstract Argumentation in Higher-Order Logic

E-print/Working paper (2021)

We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of ... [more ▼]

We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools. This enables the formal analysis and verification of meta-theoretical properties as well as the flexible generation of extensions and labellings with respect to well-known argumentation semantics. [less ▲]

rio: Reasoner for Input/Output Logics

Software (2021)

rio provides a TPTP-aligned [3] automated reasoning system for unconstrained and constrained I/O logics basid on the outi operators, 1 ≤ i ≤ 4. It is implemented as a Scala application and based on the ... [more ▼]

rio provides a TPTP-aligned [3] automated reasoning system for unconstrained and constrained I/O logics basid on the outi operators, 1 ≤ i ≤ 4. It is implemented as a Scala application and based on the scala-tptp-parser [4]. In short, the system allows you to specify a set of conditional norms and a number of inputs (each of which describing aspects of the current situational context), and provides automated means for inferring whether given obligations (also encoded as formulas) can be derived. rio can also be used to infer the set of detached obligations instead of checking detachment of given ones. [less ▲]

A Flexible Approach to Argumentation Framework Analysis using Theorem Proving

in First International Workshop on Logics for New-Generation Artificial Intelligence (2021)

Argumentation frameworks constitute the central concept of argumentation theory of Dung. In this paper we present a novel and flexible approach of analyzing argumen- tation frameworks and their semantics ... [more ▼]

Argumentation frameworks constitute the central concept of argumentation theory of Dung. In this paper we present a novel and flexible approach of analyzing argumen- tation frameworks and their semantics based on an encoding into extensional type theory (classical higher-order logic). This representation enables the use of a wide range of interactive and automated higher-order reasoning tools for assessing argu- mentation frameworks. This includes the generation of labellings (and extensions), the assessment of meta-theoretic properties, the conduction of interactive empirical experiments, and the flexible analysis of argumentation frameworks with interpreted arguments. [less ▲]

LogiKEy Workbench: Deontic Logics, Logic Combinations and Expressive Ethical and Legal Reasoning (Isabelle/HOL Dataset)

in Data in Brief (2020), 33

The LogiKEy workbench and dataset for ethical and legal reasoning is presented. This workbench simultaneously supports development, experimentation, assessment and deployment of formal logics and ethical ... [more ▼]

The LogiKEy workbench and dataset for ethical and legal reasoning is presented. This workbench simultaneously supports development, experimentation, assessment and deployment of formal logics and ethical and legal theories at different conceptual layers. More concretely, it comprises, in form of a dataset (Isabelle/HOL theory files), formal encodings of multiple deontic logics, logic combinations, deontic paradoxes and normative theories in the higher-order proof assistant system Isabelle/HOL. The data were acquired through application of the LogiKEy methodology, which supports experimentation with different normative theories, in different application scenarios, and which is not tied to specific logics or logic combinations. Our workbench consolidates related research contributions of the authors and it may serve as a starting point for further studies and experiments in flexible and expressive ethical and legal reasoning. It may also support hands-on teaching of non-trivial logic formalisms in lecture courses and tutorials. [less ▲]

Leo-III 1.5

Software (2020)

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based ... [more ▼]

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external (mostly first-order) theorem provers for increased performance. Nevertheless, Leo-III can also be used as a stand-alone prover without employing any external cooperation. In addition for its HOL reasoning capabilities, Leo-III supports reasoning in many higher-order quantified modal logics. [less ▲]

I/O Logic Workbench

Software (2020)

The I/O Logic Workbench is aimed at providing a browser-based automated reasoning system for various I/O logics. In short, the system allows you to input a set of norms and an input (the description of ... [more ▼]

The I/O Logic Workbench is aimed at providing a browser-based automated reasoning system for various I/O logics. In short, the system allows you to input a set of norms and an input (the description of the current situation), and provides automated means for inferring whether a certain formula can be derived as an obligation from this. [less ▲]

Towards an Executable Methodology for the Formalization of Legal Texts

in Dastani, Mehdi; Dong, Huimin; van der Torre, Leon (Eds.) Logic and Argumentation. CLAR 2020 (2020, March)

A methodology for the formalization of legal texts is presented. This methodology is based on features of the NAI Suite, a recently developed formalization environment for legal texts. The ability of the ... [more ▼]

A methodology for the formalization of legal texts is presented. This methodology is based on features of the NAI Suite, a recently developed formalization environment for legal texts. The ability of the tool to execute queries is used in order to drive a correct formalization until all queries are validated. The approach is studied on a fragment of the Smoking Prohibition (Children in Motor Vehicles) (Scotland) Act 2016 of the Scottish Parliament. [less ▲]

Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III

in KI – Künstliche Intelligenz (2020), 34(1), 105-108

Leo-III 1.4

Software (2019)