Automating Defeasible Reasoning in Law

TL;DR

This paper presents methods for automating defeasible reasoning in legal rule systems by translating rule modifiers into formulas and comparing classical and non-monotonic logic approaches using SMT and ASP solvers.

Contribution

It introduces rule transformations to eliminate modifiers and provides a comparative analysis of classical and non-monotonic reasoning approaches for legal norms.

Findings

Rule modifiers can be systematically eliminated through transformations.

Classical logic with SMT solvers effectively handles rule reasoning.

Non-monotonic logic with ASP offers an alternative reasoning framework.

Abstract

The paper studies defeasible reasoning in rule-based systems, in particular about legal norms and contracts. We identify rule modifiers that specify how rules interact and how they can be overridden. We then define rule transformations that eliminate these modifiers, leading in the end to a translation of rules to formulas. For reasoning with and about rules, we contrast two approaches, one in a classical logic with SMT solvers as proof engines, one in a non-monotonic logic with Answer Set Programming solvers.