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.
A defeasible theory consists of five diferent 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 .
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 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 (
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
(
Literal is definitely provable if either (
− Δ: If ( + 1) = − Δ then
(
Literal cannot be definitely proven ( − Δ) if (
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 if ∀ ∈ (), + ∈ (1..); (ii) discarded if ∃ ∈ () such that − ∈ (1..).
We now introduce the proof conditions to show that a literal is defeasibly provable.
+: If ( + 1) = + then
(
(2.3.1) ∃ ∈ [] s.t. is applicable and > .
Literal is defeasibly provable if (
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
(
(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.
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.) 1Rules are automatically labelled with a progressive number, following the inserting order: 1, 2, . . .
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.
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.
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 sufice 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.
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 diferent 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 diferent 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
We perform two experiments2 on synthetic theories and compare the two reasoners on two diferent 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 dificult 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 diferent situations and not just on a handful of cases. The details on how we proceed with this random generation are specified below. 2All 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 ifle, the conclusions and the times. 1.2 1.0 0.8 ) 0000....0246 TotalTime(s 0.2 0.10 ) 000...000468 easoningTime(s 0.02 R 0.00 Numberof6r0u0le0s800010000 0 5 10N1u5m2be0r2o5f l3it0er3al5s40 20004000 4.1. Experiment 1: diferent 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 diferent 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 diference 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
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: diferent 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 100
200 Theory index300 (a) Total time in seconds 400 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 efect 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 diferent 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 diference 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.
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 framework 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].
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 efective, 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. [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 eficient 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.