=Paper=
{{Paper
|id=Vol-3354/paper2
|storemode=property
|title=Houdini (unchained): An Effective Reasoner for Defeasible Logic
|pdfUrl=https://ceur-ws.org/Vol-3354/paper2.pdf
|volume=Vol-3354
|authors=Matteo Cristani,Guido Governatori,Francesco Olivieri,Luca Pasetto,Francesco Tubini,Celeste Veronese,Alessandro Villa,Edoardo Zorzi
|dblpUrl=https://dblp.org/rec/conf/aiia/CristaniGOPTVVZ22
}}
==Houdini (unchained): An Effective Reasoner for Defeasible Logic==
https://ceur-ws.org/Vol-3354/paper2.pdf
Houdini (unchained): an effective reasoner for
defeasible logic
Matteo Cristani1,† , Guido Governatori† , Francesco Olivieri2,† , Luca Pasetto1,† ,
Francesco Tubini1,† , Celeste Veronese1,† , Alessandro Villa1,† and Edoardo Zorzi1,3,†
1
Department of Computer Science, University of Verona, Verona, 37134, Italy
2
School of Information and Communication Technology, IIIS, Griffith University, Nathan, QLD 4111, Australia
3
Department of Computer Science, ETH Zurich, 8092 Zurich, Switzerland
Abstract
This paper introduces Houdini, a Java implementation of a propositional defeasible logic reasoner. We
discuss the development endeavoured so far. Houdini constitutes the first step in a longer plan, we
anticipate here as well, that aims at extending the implementation to treat deontic defeasible theories,
along with some relevant entities such as amounts, dates and durations. The system is presented in
terms of architecture, performance and actual functionalities for the implementation phase documented
here, and envisioned in the further steps we are in the process of carrying out in the near future.
Keywords
Defeasible logic; automated reasoning; non-monotonic reasoning.
1. Introduction
We present a novel implementation of propositional defeasible logic, called Houdini. It im-
plements a well-known method for computing extensions of propositional defeasible theories
(namely deductive closures with specific proof tags), based on a forward-chaining propagation
algorithm.
The development of Houdini presented here, version 1.0, is the first step of an implementation
plan, currently still in progress, which we shall introduce later in Section 6. The implementation
language is Java, without any database technology. A reasoner for propositional defeasible
logic named SPINdle [1] has already been developed in the past: a comparison in terms of
performance between SPINdle and Houdini can be found in Section 4.
The formal definition of the logic is provided in Section 2, while the reasoning algorithms are
presented in Section 3, along with the implementation details of the system. Section 5 discusses
related work and Section 6 takes some conclusions and sketches further work.
AI3 2022, 6th Workshop on Advances in Argumentation in Artificial Intelligence, CEUR Workshop Proceedings (CEUR-
WS.org), November 28 - December 02, 2022, Udine, Italy
†
These authors contributed equally.
$ matteo.cristani@univr.it (M. Cristani); guido@governatori.net (G. Governatori); f.olivieri@griffith.edu.au
(F. Olivieri); luca.pasetto@univr.it (L. Pasetto); francesco.tubini@univr.it (F. Tubini); celeste.veronese@univr.it
(C. Veronese); alessandro.villa@univr.it (A. Villa); edoardo.zorzi@univr.it (E. Zorzi)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
2. Defeasible logic
A defeasible theory consists of five different kinds of knowledge: facts, strict rules, defeasible
rules, defeaters, and a superiority relation [2].
Let PROP be a set of propositional atoms, Lbl be a set of arbitrary labels. The set Lit =
PROP ∪ {¬𝑝|𝑝 ∈ PROP} denotes the set of literals. The complement of a literal 𝑞 is denoted
by ∼𝑞; if 𝑞 is a positive literal 𝑝, then ∼𝑞 is ¬𝑝, and if 𝑞 is a negative literal ¬𝑝 then ∼𝑞 is 𝑝.
Definition 1. A defeasible theory 𝐷 is a structure (𝐹, 𝑅, >), where
1. 𝐹 ⊆ Lit is a set of facts that denote simple pieces of information that are always considered
to be true. For example, a fact is that “Sylvester is a cat”, formally 𝑐𝑎𝑡(𝑆𝑦𝑙𝑣𝑒𝑠𝑡𝑒𝑟);
2. 𝑅, the set of rules, contains three types of rules: strict rules, defeasible rules, and defeaters.
3. > ⊆ 𝑅 × 𝑅 is a binary relation whose transitive closure is acyclic. We refer to this relation
as superiority relaation.
A theory is finite if the set of facts and rules are finite.
A rule is an expression 𝑟 : 𝐴(𝑟) ˓→ 𝐶(𝑟) and consists of: (i) A unique name 𝑟 ∈ Lbl, (ii) the
antecedent 𝐴(𝑟) which is a finite subset of Lit (also known as the body of the rule), (iii) an arrow
˓→ ∈ {→, ⇒, ↝} denoting, respectively, a strict rule, a defeasible rule and a defeater, and (iv)
its consequent (or head) 𝐶(𝑟) ∈ Lit, which is a single literal. A strict rule is a rule in which
whenever the premises are indisputable (e.g., facts), then so is the conclusion. For example,
𝑐𝑎𝑡(𝑋) → 𝑚𝑎𝑚𝑚𝑎𝑙(𝑋)
means that “every cat is a mammal”. On the other hand, a defeasible rule is a rule that can be
defeated by contrary evidence; for example, “cats typically eat birds”:
𝑐𝑎𝑡(𝑋) ⇒ 𝑒𝑎𝑡𝐵𝑖𝑟𝑑𝑠(𝑋).
The underlying idea is that if we know that something is a cat, then we may conclude that it eats
birds unless there is evidence proving otherwise. Defeaters are rules that cannot be used to draw
conclusions directly. Their only use is to prevent some conclusions, i.e., to defeat defeasible
rules by producing evidence to the contrary. An example is “if a cat has just fed itself, then it
might not eat birds”:
𝑗𝑢𝑠𝑡𝐹 𝑒𝑑(𝑋) ↝ ¬𝑒𝑎𝑡𝐵𝑖𝑟𝑑𝑠(𝑋).
The superiority relation > among rules is used to define where one rule may override a second
rule for the (opposite) conclusion, e.g., given the defeasible rules
𝑟 : 𝑐𝑎𝑡(𝑋) ⇒ 𝑒𝑎𝑡𝐵𝑖𝑟𝑑𝑠(𝑋)
′
𝑟 : 𝑑𝑜𝑚𝑒𝑠𝑡𝑖𝑐𝐶𝑎𝑡(𝑋) ⇒ ¬𝑒𝑎𝑡𝐵𝑖𝑟𝑑𝑠(𝑋)
which would contradict one another if Sylvester is both a cat and a domestic cat, they do not in
fact contradict if we state that 𝑟′ wins against 𝑟, leading to conclude that Sylvester does not to
eat birds.
Like in [2], we consider only a propositional version of this logic, and we do not take into
account function symbols. Every expression with variables represents the finite set of its
variable-free instances.
We use the infix notation 𝑟 > 𝑠 to mean that (𝑟, 𝑠) ∈ >. The set of strict rules in 𝑅 is denoted
by 𝑅s , and the set of strict and defeasible rules by 𝑅sd . We name 𝑅[𝑞] the set of rules in 𝑅
whose head is 𝑞. A conclusion of 𝐷 is a tagged literal and can have one of the following forms:
• +Δ𝑞, which means that 𝑞 is definitely provable in 𝐷, i.e., there is a definite proof for 𝑞,
that is a proof using facts, and strict rules only;
• −Δ𝑞, which means that 𝑞 is definitely not provable, or refuted, in 𝐷 (i.e., a definite proof
for 𝑞 does not exist);
• +𝜕𝑞, which means that 𝑞 is defeasibly provable in 𝐷;
• −𝜕𝑞, which means that 𝑞 is not defeasibly provable, or refuted, in 𝐷.
Given a defeasible theory 𝐷, a proof 𝑃 of length 𝑛 in 𝐷 is a finite sequence 𝑃 (1), . . . , 𝑃 (𝑛) of
tagged literals of the type +Δ𝑞, −Δ𝑞, +𝜕𝑞 and −𝜕𝑞, where the proof conditions defined in the
rest of this section hold. 𝑃 (1..𝑛) denotes the first 𝑛 steps of proof 𝑃 .
Given # ∈ {Δ, 𝜕} and a proof 𝑃 in 𝐷, a literal 𝑞 is #-provable in 𝐷 if there is a line 𝑃 (𝑚)
of 𝑃 such that 𝑃 (𝑚) = +#𝑞. A literal 𝑞 is #-refuted in 𝐷 if there is a line 𝑃 (𝑚) of 𝑃 such
that 𝑃 (𝑚) = −#𝑞.
The Definition of Δ describes just forward chaining of strict rules.
+Δ: If 𝑃 (𝑛 + 1) = +Δ𝑞 then
(1) 𝑞 ∈ 𝐹 or
(2) ∃𝑟 ∈ 𝑅𝑠 [𝑞]∀𝑎 ∈ 𝐴(𝑟) : +Δ𝑎 ∈ 𝑃 (1..𝑛).
Literal 𝑞 is definitely provable if either (1) is a fact, or (2) there is a strict rule for 𝑞, whose
antecedents have all been definitely proved.
−Δ: If 𝑃 (𝑛 + 1) = −Δ𝑞 then
(1) 𝑞 ∈
/ 𝐹 and
(2) ∀𝑟 ∈ 𝑅𝑠 [𝑞]∃𝑎 ∈ 𝐴(𝑟) : −Δ𝑎 ∈ 𝑃 (1..𝑛).
Literal 𝑞 cannot be definitely proven (−Δ𝑞) if (1) is not a fact and (2) every strict rule for 𝑞 has
at least one definitely refuted antecedent.
The following definition gives the conditions for when a rule is applicable or discarded.
Definition 2. In the proof condition for ±𝜕, a rule 𝑟 ∈ 𝑅𝑠𝑑 is (i) applicable iff ∀𝑎 ∈ 𝐴(𝑟),
+𝜕𝑎 ∈ 𝑃 (1..𝑛); (ii) discarded iff ∃𝑎 ∈ 𝐴(𝑟) such that −𝜕𝑎 ∈ 𝑃 (1..𝑛).
We now introduce the proof conditions to show that a literal is defeasibly provable.
+𝜕: If 𝑃 (𝑛 + 1) = +𝜕𝑞 then
(1) +Δ𝑞 ∈ 𝑃 (1..𝑛) or
(2) (2.1) −Δ∼𝑞 ∈ 𝑃 (1..𝑛) and
(2.2) ∃𝑟 ∈ 𝑅sd [𝑞] s.t. 𝑟 is applicable, and
(2.3) ∀𝑠 ∈ 𝑅[∼𝑞]. either 𝑠 is discarded, or
(2.3.1) ∃𝑡 ∈ 𝑅[𝑞] s.t. 𝑡 is applicable and 𝑡 > 𝑠.
Literal 𝑞 is defeasibly provable if (1) 𝑞 is already definitely provable, or (2) we argue using the
defeasible part of the theory. For (2), ∼𝑞 is not definitely provable (2.1), and there exists an
applicable strict or defeasible rule for 𝑞 (2.2). Every attack 𝑠 is either discarded (2.3), or defeated
by a stronger rule 𝑡 (2.3.1). When, specifically, no attack exists, namely the literal is supported
and there is no support for the opposite literal, then we say that the literal is irrefutable.
On the other hand, to prove the a literal is defeasibly refuted (−𝜕) we have to show that all
possible ways to prove it fail. This is encoded by the following proof conditions that correspond
to a constructive negation of the conditions for +𝜕.
−𝜕: If 𝑃 (𝑛 + 1) = −𝜕𝑞 then
(1) −Δ𝑞 ∈ 𝑃 (1..𝑛) and either
(2) (2.1) +Δ∼𝑞 ∈ 𝑃 (1..𝑛) or
(2.2) ∀𝑟 ∈ 𝑅sd [𝑞]. either 𝑟 is discarded, or
(2.3) ∃𝑠 ∈ 𝑅[∼𝑞] s.t. 𝑠 is applicable, and
(2.3.1) ∀𝑡 ∈ 𝑅[𝑞]. either 𝑡 is discarded, or 𝑡 ̸> 𝑠.
Given # ∈ {Δ, 𝜕}, a literal 𝑝 and a theory 𝐷, we use 𝐷 ⊢ ±#𝑝 to denote that there is a
proof 𝑃 in 𝐷 where for some line 𝑖, 𝑃 (𝑖) = ±#𝑝. Alternatively, we say that ±#𝑝 holds in
𝐷, or simply ±#𝑝 holds when the theory is clear from the context. The set of positive and
negative conclusions is called extension. Formally,
Definition 3. Given a defeasible theory 𝐷, the extension of 𝐷 is defined as 𝐸(𝐷) =
(+Δ, −Δ, +𝜕, −𝜕), where ±# = {𝑙 : 𝑙 appears in 𝐷 and 𝐷 ⊢ ±#𝑙}, # ∈ {Δ, 𝜕}. We
refer to (+Δ, −Δ) as the Definite extension and (+𝜕, −𝜕) as the Defeasible extension.
3. The implementation of Houdini
Houdini is a Spring based web application written in Java. Its architecture consists of three
major components: a User Interface, a Parser (which also works as a validator module) and a
Reasoner.
As shown in Figure 1, inputs (that is, defeasible logic theories) can be provided to the system
through an interactive front-end user interface, either by inserting plain text in the embedded
dynamic web-form, or by directly uploading a JSON file (see Figure 2 for a preview of the
interface). In the first case, the collection of plain text elements is converted into a JSON
structure anyway, in order to give the result to the parser for validation, whereas in the second
case the file data is directly fed to the module. Be that as it may, the accepted syntax is the same.
The user can provide three types of information: facts, syntactically just single literals (so,
any custom alphanumerical string with in addition the character ‘_’ and ‘~’, which can only
be prefixed to interpret it as a negation), rules, specific strings divided into an optional body
(comma-separated sequence of literals, or a single literal), an arrow (defining the nature of the
rule) and the head (non-optional single literal), and instances of the superiority relation (simply
two rule names1 separated by a ‘>’ character, where the left-side one is the superior rule, and
the right-side one is instead the inferior rule.)
1
Rules are automatically labelled with a progressive number, following the inserting order: 𝑟1, 𝑟2, . . .
Figure 1: Houdini’s architecture and data flow
Figure 2: Houdini’s front-end offers two ways to provide a theory
After the input is submitted, the parser module obtains the JSON structure and, at first,
checks its overall syntactic validity; then, it proceeds to build the object-oriented internal
theory representation which will be processed by the reasoner to compute the strict and partial
extensions. Algorithm 1 shows the reasoner’s workflow.
Algorithm 1 Reasoner
Require: JSONData
1: Theory ← ParserValidator(JSONData)
2: (Theory′ , Extension′ ) ← StrictReasoner(Theory)
3: (Theory′′ , Extension′′ ) ← DefeasibleReasoner(Theory′ , Extension′ )
4: return Extension′′
The user input is processed by an ANTLR standard CFG parser, which validates the data and
builds the theory object, later fed to the reasoner modules.
Figure 3 shows the main fields of the Literal and Rule classes. Each literal object contains
two sets of rule labels: those referring to rules in which the literal is part of the body, and those
referring to rules where the head is the literal. These fields are very useful to guarantee direct
access to the rules which are very frequently checked in the reasoning process.
Figure 3: Main attributes of the Literal and Rule classes
The reasoner operates in two modules: Strict Reasoner and Defeasible Reasoner.
Strict Reasoner (Algorithm 2) computes +Δ and −Δ and follows an injection strategy to find
literals that ought to be added to the definite extension. It starts from the facts, guaranteed to
be in +Δ, and removes them from all bodies of rules they’re part of. Eventually, new injectable
literals are found (heads of completely activated strict rules, i.e. with empty bodies) and the
process continues until no new literals are added to the injectable set: when this happens,
+Δ has been completely determined. Then it starts from all those literals that are neither
facts nor heads of strict rules (guaranteed to be in −Δ) and starts an analogous process to
completely build −Δ. Defeasible Reasoner (Algorithm 3), instead, computes +𝜕 and −𝜕. It
starts by restricting the set of the remaining undecided literals and then checks, for each of
them, the membership conditions for the two sets. When it finds one of them, it either injects it
into the rules or it deactivates it, but, unlike Strict Reasoner, this does not suffice for adding
their heads directly to an injectable or deactivation sets. Note that the algorithm loops over the
candidates (after having adequately updated them) until the fixed point is reached: this happens
when, after an entire loop, no literal has been added to either set; in this case the algorithm
ends and returns the conclusions.
Figure 4: Houdini’s front end: computation of the extensions.
4. Performance evaluation
Computing the extension of a propositional defeasible theory can be computed in linear time
[3]. After running multiple tests on Houdini’s correctness by cross-checking its conclusions
results against a test bench of miscellaneous theories encompassing multiple facets of reasoning
and corner cases, we test its performances by comparing them with those of SPINdle. SPINdle is
a state-of-art implementation of Defeasible Logic that implement different variants of the logic.
Recent experiments report that SPINdle outperforms some other implementations of defeasible
reasoning [4, 5] and it is comparable to other highly optimised non-monotonic reasoning engines
[6]. Furthemore, SPINdle has been successfully used in defeasible logic based applications (in
the legal domain) [7, 8]. SPINdle is a Java implementation of defeasible logic that generates the
extension of a defeasible theory. The implementation is similar to the implementation presented
in this paper with some different choices to prevent performance issues, especially in terms of
space occupancy.
Algorithm 2 Strict Extension
Require: Theory ◁ Fed by the validator & parser module
1: StrictReasoner(Theory)
2:
3: function StrictReasoner(Theory)
4: Extension ← ∅ ◁ All sets (+Δ, −Δ, +𝜕, −𝜕) are, at first, empty
5: toInject ← {𝑙 ∈ ℒ | 𝑙 ∈ ℱ} ◁ All literals that are facts
6: toDeactivate ← {𝑙 ∈ ℒ | 𝑙 ̸∈ ℱ ∧ 𝑅𝑠 [𝑙] = ∅} ◁ Literals not facts nor heads of strict rules
7: for 𝑙 in toInject do ◁ If the set is empty it doesn’t run
8: InjectLiteral(𝑙, toInject, Theory, Extension)
9: end for
10: for 𝑙 in toDeactivate do ◁ If the set is empty it doesn’t run
11: DeactivateLiteral(𝑙, toDeactivate, Theory, Extension)
12: end for
13: return Theory, Extension
14: end function
15:
16: function InjectLiteral(𝑙, toInject, Theory, Extension)
17: for r ∈ 𝑅[𝑙 ∈ body] do ◁ All rules with 𝑙 in their bodies
18: Remove 𝑙 from 𝑟.body (update Theory)
19: if 𝑟.body = ∅ then
20: 𝑟.tag ← Activated
21: if 𝑟 ∈ 𝑅𝑠 then ◁ Must also be a strict rule
22: Add 𝑟.head to toInject
23: end if
24: end if
25: end for
26: Remove 𝑙 from toInject and add it to +Δ and +𝜕 (update Extension)
27: end function
28:
29: function DeactivateLiteral(𝑙, toDeactivate, Theory, Extension)
30: for r ∈ 𝑅[𝑙 ∈ body] do
31: 𝑟.tag ← StrictlyDeactivated (update Theory)
32: if ∀𝑡 ∈ 𝑅𝑠 [𝑟.head] 𝑡.tag = StrictlyDeactivated then *
33: Add 𝑟.head to toDeactivate
34: end if
35: end for
36: Remove 𝑙 from toDeactivate and add it to −Δ (update Extension)
37: end function
38: *: If, after ‘deactivating’ a rule 𝑟 with 𝑙 in the body we find that, for its head 𝑞, this was the last ‘not
deactivated’ rule in 𝑅𝑠 [𝑞], add 𝑞 to the literals to be deactivated
Algorithm 3 Defeasible Extension
Require: Theory, Extension
1: DefeasibleReasoner(Theory, Extension)
2:
3: function DefeasibleReasoner(Theory, Extension)
4: PlusPartialCandidates ← {𝑙 ∈ ℒ | 𝑙 ̸∈ +Δ ∧ ~𝑙 ∈ −Δ} ◁ Candidates not already in +𝜕
5: MinusPartialCandidates ← {𝑙 ∈ ℒ | 𝑙 ∈ −Δ}
6: do
7: fixedPoint ← true
8: for 𝑙 in PlusPartialCandidates do
9: if ∃𝑟 ∈ 𝑅𝑠𝑑 [𝑙] s.t. 𝑟.tag = Activated then
10: isPartial ← true
11: for t ∈ 𝑅[~𝑙] s.t. 𝑡.tag ̸= DefeasiblyDeactivated do
12: versus ← {𝑠 ∈ 𝑅𝑠𝑑 [𝑙] | 𝑠 > 𝑡}
13: if versus = ∅ ∨ ∄𝑠 ∈ versus s.t. 𝑠.tag = Activated then
14: isPartial ← false
15: break
16: end if
17: end for
18: if isPartial = true then
19: injectLiteral(l, Theory, Extension)
20: Remove 𝑙 from both candidates sets
21: fixedPoint ← false
22: end if
23: end if
24: end for
25: for 𝑙 in MinusPartialCandidates do
26: if ∀𝑟 ∈ 𝑅𝑠𝑑 [𝑙] 𝑟.tag = DefeasiblyDeactivated ∨ ~𝑙 ∈ +Δ then
27: DeactivateLiteral(l, Theory, Extension)
28: Remove 𝑙 from both candidates sets
29: fixedPoint ← false
30: end if
31: isPartial ← false
32: for 𝑡 ∈ 𝑅[~𝑙] s.t. 𝑡.tag = Activated do
33: versus ← {𝑠 ∈ 𝑅𝑠𝑑 [𝑙] | 𝑠 > 𝑡}
34: if versus = ∅ ∨ ∀𝑠 ∈ versus, 𝑠.tag = DefeasiblyDeactivated then
35: isPartial ← true
36: break
37: end if
38: end for
39: if isPartial = true then
40: DeactivateLiteral(l, Theory, Extension)
41: Remove 𝑙 from both candidates sets
42: fixedPoint ← false
43: end if
44: end for
45: while fixedPoint = false
46: return Theory, Extension
47: end function
48: (Continue)
49: (Cont’d)
50: function InjectLiteral(𝑙, Theory, Extension)
51: for r ∈ 𝑅[𝑙 ∈ body] do ◁ All rules with 𝑙 in their bodies
52: Remove 𝑙 from 𝑟.body (update Theory)
53: if 𝑟.body = ∅ then
54: 𝑟.tag ← Activated
55: end if
56: end for
57: Add 𝑙 to +𝜕 (update Extension)
58: end function
59:
60: function DeactivateLiteral(𝑙, Theory, Extension)
61: for r ∈ 𝑅[𝑙 ∈ body] do
62: 𝑟.tag ← DefeasiblyDeactivated (update Theory)
63: end for
64: Add 𝑙 to −𝜕 (update Extension)
65: end function
We perform two experiments2 on synthetic theories and compare the two reasoners on two
different time statistics: the total time in seconds, i.e., the interval spanning from the start of
the loading and parsing phase to the end of the reasoning phase (after which the conclusions
are outputted to the user); and the reasoning time in seconds, which includes only the latter.
In the first experiment, we compare the two reasoners across multiple theories varying in size
(both the number of rules and the number of literals), whereas in the second experiment we fix
the size but we change, randomly, the facts of the theories. These tests have been performed to
isolate the performances of Houdini for fixed rule sets, in the perspective of devising a deontic
system, where rules represent the normative background and facts the actual events that the law
may be governing.
To have meaningful results and, in particular, to assess the performance of the two reasoners
in a variety of real-world conditions, the theories are generated randomly and yet always
following a certain structure, akin to that of many theories that would stem from user inputs or
common use cases. In doing so, we generate a copious amount of tests (which would be difficult
with hand-wrought theories) that also vary greatly in their extensions (that is, such that their
conclusions sets and +𝜕, in particular, are not trivial and vary a lot from theory to theory); this
is important because it guarantees that the tests are performed on many different situations
and not just on a handful of cases. The details on how we proceed with this random generation
are specified below.
2
All tests have been performed locally on a 8GB memory machine, 3.40 Ghz Intel i5, and Ubuntu 18.04 LTS. The
Houdini tests have been run in Java 11 whereas the SPINdle ones (version 2.2.4) using Java 8. We completely
bypassed any user interface and directly fed theories (in the correct format) to both reasoners, saving, in an external
file, the conclusions and the times.
SPINdle SPINdle
Houdini Houdini
1.2
1.0 0.10
Reasoning Time(s)
0.8 0.08
Total Time(s)
0.6 0.06
0.4 0.04
0.2
0.02
0.0
0.2 0.00
2000 35 40 2000 35 40
Num4000 6000 25 30 ls Num4000 25 30 ls
ber o
f rule 8000 10 15 20 of litera ber 6000
of ru 8000 15 20 of litera
b e r 10 be r
s 10000 0 5 Num les
10000 0 5 Num
(a) Total time in seconds (b) Reasoning time in seconds
Figure 5: Scatterplot of mean times in seconds (total time and reasoning time only) for SPINdle and
Houdini on 25 hyperparameters. The planes are fitted with a normal linear regression on the parameters.
4.1. Experiment 1: different sizes
Given the two parameters 𝑛, the number of rules, and 𝑤, the ‘width’, i.e. the number of literals
making up the body of any rule (fixed across the whole theory) proceed as follows: starts
with 𝑤 active empty body rules: {𝑟0 : ⇒ 𝑏0 , . . . , 𝑟𝑤−1 : ⇒ 𝑏𝑤−1 } and then, until the theory
comprises of 𝑛 rules, add 𝑟𝑖 whose body is made of 𝑤 randomly sampled (without replacement)
literals taken from {𝑏0 , . . . , 𝑏𝑖−1 } (i.e. heads of previous rules) and head 𝑏𝑖 . With probability
𝑝𝑐, set the first literal in the body as 𝑋, a literal guaranteed to be defeasibly unprovable, and,
independently, with probability 𝑝𝑠, add another rule 𝑟𝑖+1 with a different body and head ∼ 𝑏𝑖 ,
setting randomly either 𝑟𝑖+1 > 𝑟𝑖 or 𝑟𝑖+1 < 𝑟𝑖 as superiority relation. To limit the sparseness
of the theory, after a threshold 𝑐 the heads will loop over and repeat: for rule 𝑟𝑖 , 𝑖 > 𝑐 the head
will be 𝑏𝑗 where 𝑗 ≡ 𝑖 (mod 𝑐).
This procedure generates a random theory that is not completely dissimilar to theories that
would derive from real-world situations. In particular, the initial rules are more likely to be
activated than later ones, because of a smaller pool of heads to choose from for their bodys, and
their activation status depends more on the status of rules that immediately precede them.
The main difference between theories generated this way resides in the randomly inserted
unprovable literals 𝑋 that break ‘derivation chains’ that, otherwise, would go from the first
rule to the last one and would always lead to the same conclusions.
We set 𝑁 = {1000, 2500, 5000, 7500, 10000}, 𝑊 = {8, 16, 24, 32, 40}, 𝑝𝑐 = 𝑝𝑠 = 0.0025
and 𝑐 = 200 and generate 20 random theories (as in Section 4.1) for each parameter (𝑛, 𝑤) ∈
𝑁 × 𝑊 . So, in total, we test the two reasoners over 500 theories, 20 theories for 25 combinations
of hyperparameters.
For 𝑝𝑐 and 𝑝𝑠 percentages are low to avoid theories with too small or large conclusions sets;
in particular, we want to avoid both the case where +𝜕 is only made up of the first 𝑤 literals
𝑏0 , . . . , 𝑏𝑤−1 and the case where +𝜕 includes everything but 𝑋. If the probabilities were too
high, we would have the first case, if the probabilities were too small, the second one.
#Rules Width Total Time Reasoning Time
Houdini SPINdle Improvement Houdini SPINdle Improvement
1000 8 0.0468 0.0763 1.63x 0.0046 0.0174 3.75x
1000 16 0.0307 0.0722 2.35x 0.0038 0.0151 3.94x
1000 24 0.0365 0.0946 2.60x 0.0050 0.0169 3.36x
1000 32 0.0460 0.1247 2.71x 0.0056 0.0247 4.37x
1000 40 0.0579 0.1022 1.76x 0.0096 0.0176 1.84x
2500 8 0.0298 0.1627 5.46x 0.0017 0.0399 22.83x
2500 16 0.0526 0.1516 2.88x 0.0037 0.0204 5.43x
2500 24 0.0842 0.2013 2.39x 0.0060 0.0239 3.96x
2500 32 0.1168 0.2621 2.24x 0.0094 0.0348 3.69x
2500 40 0.1393 0.3402 2.44x 0.0136 0.0609 4.50x
5000 8 0.0605 0.2070 3.42x 0.0030 0.0375 12.31x
5000 16 0.1179 0.2926 2.48x 0.0067 0.0396 5.92x
5000 24 0.1704 0.3989 2.34x 0.0111 0.0483 4.33x
5000 32 0.2321 0.5032 2.17x 0.0177 0.0582 3.29x
5000 40 0.2872 0.6180 2.15x 0.0255 0.0759 2.97x
7500 8 0.1001 0.3163 3.16x 0.0047 0.0565 12.03x
7500 16 0.1762 0.4391 2.49x 0.0120 0.0598 4.97x
7500 24 0.2703 0.5915 2.19x 0.0162 0.0680 4.18x
7500 32 0.3729 0.7387 1.98x 0.0240 0.0688 2.87x
7500 40 0.4680 0.8999 1.92x 0.0273 0.0824 3.02x
10000 8 0.1283 0.4328 3.37x 0.0066 0.0775 11.75x
10000 16 0.2380 0.5854 2.46x 0.0171 0.0780 4.56x
10000 24 0.3735 0.7789 2.09x 0.0226 0.0861 3.81x
10000 32 0.5330 0.9655 1.81x 0.0257 0.0864 3.36x
10000 40 0.6664 1.1684 1.75x 0.0292 0.1097 3.76x
Table 1
Mean times, in seconds, for SPINdle and Houdini with respect to experiment 1.
Results are reported kin Figure 5 and Table 1. Houdini consistently outperforms SPINdle in
both statistics. The gains are more sizeable when we consider only the reasoning time (right
image, second half of the table): depending on the hyperparameters, we go from just under 2
times faster to up to around 23 times faster; if we do not consider outliers, the improvements are
consistently in the 3-4.5x range. For the total time, these somewhat decrease to around 2x: this
is consistent with the fact that Houdini has an heavy initialization phase, more so than SPINdle,
due to most of the computational improvements and ‘tricks’ requiring saving and manipulating
lots of information before the reasoning phase; moreover, this makes Houdini more memory
intensive than SPINdle: we can say that we have found it to be around 1.5x to 2.5x heavier.
Improving the parsing strategy, streamlining data structures and devising more sophisticated
data management strategies are all avenues that have been considered exploring in the future.
4.2. Experiment 2: different initial hypotheses
The second test suite compares Houdini and SPINdle across theories generated following a
slight variation of the random theory generation as in Section 4.1. We call them random theories
0.45
0.12 Reasoner
0.40 SPINdle
Houdini
0.35 0.10
0.30 0.08
Reasoning Time(s)
Total Time(s)
0.25 Reasoner
SPINdle 0.06
0.20 Houdini
0.15 0.04
0.10
0.02
0.05
0.00 0.00
100 200 300 400 500 100 200 300 400 500
Theory index Theory index
(a) Total time in seconds (b) Reasoning time in seconds
Figure 6: Times in seconds (total time and reasoning time only) for SPINdle and Houdini on 500 random
theories with randomly injected hypotheses. In the x-axis the theory index, while in the y-axis the
results of that theory. The crosses on the y-axes (note the different scales) mark the mean times.
with random hypotheses. We fix 𝑛 = 10000 and 𝑤 = 5 and do the following: randomly
pick 𝑡 indexes (with no substitution) ranging from 0 to 𝑛𝑖 , {𝑖′0 , . . . , 𝑖′𝑡−1 }, and start with rules
𝑟0 : ⇒ 𝑏𝑖′0 , . . . , 𝑟𝑡−1 : ⇒ 𝑏𝑖′𝑡−1 ; then, from index 𝑖𝑛𝑖 onwards proceed before, i.e. generate rules
whose bodys comprise previously generated heads until 𝑛 rules are added. Basically, this has
the effect of injecting 𝑡 random heads, out of 𝑛𝑖 , as initial hypotheses.
We generate 500 theories fixing 𝑡 = 27 and 𝑛𝑖 = 30 so for each theory there are 3 initial
heads missing from the injected hypotheses. These numbers have been empirically chosen
to limit the sparseness of the theories (the fewer the hypotheses, the more likely it is that
the conclusions are trivial, in particular, that +𝜕 is empty excluding the hypotheses) and to
guarantee a good variety of conclusions so that the reasoners may be compared across different
situations; also, because of this initial randomness, we set 𝑝𝑐 = 𝑝𝑠 = 0.
In both scatterplots of Figure 6 we can see how Houdini is faster than SPINdle with and
without considering the loading phase. In the first case, Houdini shows a higher variance
than SPINdle, but still completely outperforms it: a mean total time of 0.088s versus 0.35s,
around 4 times faster. The results considering the reasoning time only are even better: with less
variance, Houdini takes an average of 0.005s (5ms) whereas SPINdle 0.068s (68ms), that is, a
13.6x improvement. Of note, execution times are separated: Houdini’s worst case is well below
SPINdle’s best one.
As claimed in Section 4.1, this difference in the results is due to the heavier initialization
phase; however, in this case, we perform comparatively better than in the first experiment: the
memory penalty has been consistent in the 1.25x to 1.5x range.
5. Related work
A number of investigations have been carried out in the past thirty years regarding algorithms
for propositional defeasible logic, starting with the pioneering work of Nute [9] through the
technical investigations on algorithmic methods [10] towards extensions to the logical frame-
work that include deontic operators by Nute [11]. As we discussed before SPINdle proved
very successful and superseded previous implementations. After the making of SPINdle a few
alternatives/extensions have been proposed with the key focus on large-scale reasoning with
instances. [12] proposed a map-reduce parallelisation-based implementation of the algorithm
used by SPINdle, while [13] advance a simplified version of the logic to make it more suitable to
the parallel implementation. [14] investigates a grounder for SPINdle. However, it is not clear
whether such approaches really provide advancements in terms of performance over SPINdle
in combination with relational database and related query technology [7, 15].
The most relevant application fields of (deontic) defeasible logic are indeed Legal Reasoning,
and Argumentation Analysis. It has been shown that, within the notion of argumentation there
is room for a specific semantics of Defeasible Propositional logic in terms of arguments [16].
A related formalism is Defeasible Logic Programming (DeLP) as studied by Leiva et al. [17],
that has been implemented by Gàrcia and Simari [18], also in an incremental way by Alfano et
al. [19].
6. Conclusions and further work
We have introduced a technology that computes positive (and negative) strict (and defeasible)
extensions of a propositional defeasible theory. The technology has been compared to SPINdle,
an existing technology. Performances are better, thanks to a careful analysis of drawbacks of
SPINdle, overwhelmed in Houdini. The implementation has the following characteristics:
• It provides a web-based interface implemented with a REST/SOAP approach. This can be
invoked by a regular web browser, and works on an exposed platform;
• The solution can be accessed also as an API, and it is available on GitHub, in its current
version (beta for the moment);
• The solution is effective, as it performs linearly in literals and rules;
• The solution is more performant than SPINdle, being between 2 and 3 times speeder.
The current version of Houdini, 1.0, works on propositional logic. There are some further
improvements and features that we are in the process to add. Current implementation plan
includes to extend the reasoner to deal with defeasible deontic logic, to add numerical variables
such as time and money and to implement support for LegalRuleML-formatted data.
References
[1] H.-P. Lam, G. Governatori, The making of SPINdle, in: G. Governatori, J. Hall, A. Paschke
(Eds.), Rule Representation, Interchange and Reasoning on the Web, number 5858 in LNCS,
Springer, 2009, pp. 315–322.
[2] G. Antoniou, D. Billington, G. Governatori, M. J. Maher, Representation results for defeasi-
ble logic, ACM Transactions on Computational Logic 2 (2001) 255–287.
[3] M. J. Maher, Propositional defeasible logic has linear complexity, Theory and Practice of
Logic Programming 1 (2001) 691–711.
[4] S. Batsakis, G. Baryannis, G. Governatori, T. Ilias, G. Antoniou, Legal representation and
reasoning in practice: A critical comparison, in: M. Palmirani (Ed.), Jurix 2019, IOS Press,
2018, pp. 31–40.
[5] A. Hecham, M. Croitoru, P. Bisquert, A first order logic benchmark for defeasible reasoning
tool profiling, in: C. Benzmüller, F. Ricca, X. Parent, D. Roman (Eds.), Rules and Reasoning,
RuleML+RR, LNCS 11092, Springer, 2018, pp. 81–97.
[6] L. Robaldo, S. Batsakis, R. Callegari, F. Calimeri, M. Fujita, G. Governatori, M. C. Morelli,
G. Pisano, K. Satoh, I. Tachmazidis, Taking stock of available technologies for compliance
checking on first-order knowledge, in: R. Callegari, G. Ciatto, A. Omicini (Eds.), CILC
2022: Italian Conference on Computational Logic, CEUR 3204, 2022.
[7] M. B. Islam, G. Governatori, RuleRS: A rule-based architecture for decision support systems,
Artificial Intelligence and Law 26 (2018) 315–344.
[8] G. Governatori, The Regorous approach to process compliance, in: 2015 IEEE 19th
International Enterprise Distributed Object Computing Workshop, IEEE Press, 2015, pp.
33–40.
[9] D. Nute, Defeasible logic, in: Handbook of Logic in Artificial Intelligence and Logic
Programming, 1994.
[10] G. Antoniou, D. Billington, G. Governatori, M. J. Maher, A. Rock, A family of defeasible
reasoning logics and its implementation, in: ECAI 2000, 2000, pp. 459–463.
[11] D. Nute, Norms, priorities, and defeasible logic, in: P. McNamara, H. Prakken (Eds.),
Norms, Logics and Information Systems, IOS Press, Amsterdam, 1998, pp. 201–218.
[12] I. Tachmazidis, G. Antoniou, G. Flouris, S. Kotoulas, L. McCluskey, Large-scale parallel
stratified defeasible reasoning, in: L. D. Raedt, C. Bessiere, D. Dubois, P. Doherty, P. Frasconi,
F. Heintz, P. J. F. Lucas (Eds.), ECAI 2012, volume 242, IOS Press, 2012, pp. 738–743.
[13] M. J. Maher, I. Tachmazidis, G. Antoniou, S. Wade, L. Cheng, Rethinking defeasible
reasoning: A scalable approach, Theory and Practice of Logic Programming 20 (2020)
552–586.
[14] M. Rohaninezhad, S. M. Arif, S. Azman Mohd Noah, A grounder for spindle defeasible
logic reasoner, Expert Systems with Applications 42 (2015) 7098–7109.
[15] Q. Liu, M. B. Islam, G. Governatori, Towards an efficient rule-based framework for legal
reasoning, Knowledge Base Systems 224 (2021) 107082.
[16] G. Governatori, M. J. Maher, D. Billington, G. Antoniou, Argumentation semantics for
defeasible logics, Journal of Logic and Computation 14 (2004) 675–702.
[17] M. A. Leiva, A. J. García, P. Shakarian, G. I. Simari, Argumentation-based query answering
under uncertainty with application to cybersecurity, Big Data Cogn. Comput. 6 (2022).
[18] A. García, G. Simari, Defeasible logic programming: An argumentative approach, Theory
and Practice of Logic Programming 4 (2004) 95–138. doi:10.1017/s1471068403001674.
[19] G. Alfano, S. Greco, F. Parisi, G. Simari, G. Simari, An incremental approach to structured
argumentation over dynamic knowledge bases, 2018, pp. 78–87.