Automating Defeasible Reasoning in Law with Answer Set Programming

tags

Rules as Code

Notes

On the demand side, there is a growing number of human-machine or machine-machine interactions where compliance with legal norms or with a contract is essential

NOTER_PAGE: (1 . 0.5045691906005222)

On the supply side, decisive advances have been made in fields such as automated reasoning and language technologies

NOTER_PAGE: (1 . 0.6031331592689295)

law texts are formalised in a DSL called L4

NOTER_PAGE: (1 . 0.685378590078329)

sufficiently close to a traditional law text with its characteristic elements such as cross references, prioritisation of rules and defeasible reasoning

NOTER_PAGE: (2 . 0.11031331592689295)

Classical, monotonic logic has received surprisingly little attention in this area, even though proof support in the form of SAT/SMT solvers has made astounding progress in recent years.

NOTER_PAGE: (2 . 0.3381201044386423)

defeasibility operators via encodings in Answer Set Programming (ASP) which has only negation as failure, interpreted under the stable model semantics

NOTER_PAGE: (2 . 0.4013157894736842)

do not permit for human intervention in the proof process, which would not be adequate for the user group we target

NOTER_PAGE: (2 . 0.6292428198433421)

Turnip system that is based on a combination of defeasible and deontic logic

NOTER_PAGE: (2 . 0.6892950391644909)

The purpose of our formalization efforts is to be able to make assertions and prove them, such as the statement in Figure 2 which claims that the predicate maxSp behaves like a function

NOTER_PAGE: (3 . 0.7543071161048689)

We will concentrate on two rule modifiers that restrict the applicability of rules and that frequently occur in law texts: subject to and despite

NOTER_PAGE: (4 . 0.21123595505617979)

present how some core legal reasoning tasks can be implemented in ASP while keeping the ASP representation readable and intuitive and respecting the idea of having an ‘isomorphism’ between the rules and the encoding

NOTER_PAGE: (5 . 0.1955056179775281)

The ASP based and SMT based approaches are complimentary to each other

NOTER_PAGE: (9 . 0.5543071161048689)

ASP’s closed-world assumption is useful when a legal verdict must be reached with potentially incomplete information

NOTER_PAGE: (9 . 0.5558052434456929)

when one does model checking or wants to reason about meta-properties of the rules such as soundness of the rule-set, the SMT solver approach is more suited than the ASP approach. Intuitively, here we want to reason over all possible scenarios rather than restricting the reasoning to a particular scenario being considered.

NOTER_PAGE: (9 . 0.6674157303370787)