Scalable Defeasible Reasoning

SCADR

An investigation into the scalability of practical KLM-style defeasible reasoning.

Introduction

Knowledge Representation and Reasoning (KRR) is an area of artificial intelligence which focuses on encoding knowledge about the world so that reasoning about it may be automated. This allows machines to mimic, to an varying degree of accuracy, the logical thought processes harnessed by rational animals, e.g., humans, and thus produce logical conclusions. For example, if our knowledge base comprises "penguins are birds" and "Tweety is a penguin", we can logically conclude that Tweety is a bird.

Classical reasoning operates under the assumption that the knowledge base is complete, in that each piece of knowledge is absolute. This means that previously possible inferences can not be retracted on the introduction of new knowledge. This is the property of monotonicity and causes reasoning to become unreliable when a contradiction is introduced into the knowledge base.

Defeasible reasoning centers around reasoning with incomplete knowledge. The KLM-approach is a framework for defeasible reasoning from which automated defeasible reasoning algorithms have been produced, e.g., Rational Closure and Lexicographic Closure. While theoretical work drawing from the KLM-approach is steadily increasing, little has been done in investigating practical implementations of these algorithms, and thus we present one such investigation, SCADR.

Background

Rational Closure

Rational Closure is the most conservative form of defeasible reasoning. It can be computed as follows.

Given a knowledge base, put statements in ranks depending on how general they are. (Higher up = more general). To check if a knowledge base entails that "penguins typically have wings", remove ranks one by one from the top down until its possible for penguins to exist in our world. Return true if the statements in the remaining ranks mean that penguins always have wings.

Lexicographic Closure

Lexicographic Closure works similarly to Rational Closure, however it is not necessary to remove every statement in a rank. Lexicographic Closure removes as few statements as possible, by only removing statements one at a time until the premise of our defeasible claim is consistent with our knowledge base.

The Problem

Prior to our research, there existed no implementation of KLM-style defeasible reasoning in propositional logic. There was also thus very little research done regarding the computational scalability of the algorithms to reason according to these approaches. There also lacked a mature tool for generating knowledge bases according to specified parameters.

Objectives

  • To prototype a reasoner tool which reasons about defeasible knowledge bases according to rational closure. (Hamilton)
  • To improve the scalability of such a rational closure implementation through the use of optimisation approaches. (Hamilton)
  • To develop a prototype reasoner to perform entailment checking of defeasible knowledge bases according to lexicographic closure. (Park)
  • To improve the scalability of such a lexicographic closure implementation through the use of optimisation approaches. (Park)
  • To implement an experimental tool for the generation of knowledge bases to be used for reasoner testing purposes. (Bailey)
  • To determine which factors contribute towards the number of ranks and the distribution of statements over the ranks in a ranked knowledge base. (Bailey)

Rational Closure Optimisations

The approaches taken to optimise Rational Closure were the following.

Binary Search Optimisation

We perform a binary search to find the rank from which all ranks above need to be removed. This significantly better than the linear search which is done in the original Rational Closure algorithm.

Rank Storing

We store the rank number at which a given premise becomes consistent with our knowledge base, and thus if we receive a query with the same premise, we don't need to recalculate which ranks to exclude.

Methods and Testing

A naive implementation, as well as implementations aligned with both of these optimisation approaches were developed.

These implementations' execution times were tested against each other for a given set of defeasible statements, and given knowledge bases. Knowledge base and query set characteristics such as rank at which the queries become consistent, and number of ranks, were controlled.

The reasoner was developed using Java, the source code of which can be found at the link below.

GitHub Repository

Lexicographic Closure Optimisations

It can be assumed that there are many factors that affect the performance of Lexicographic Closure Reasoner. The first optimisation step was taken by investigating the property of power set.

Definition 3.1 (Power set). A power set of 𝒜 is the set of all subsets of the set 𝒜 including the set itself and the null or empty set, denoted as 𝒫(𝒜). As an example, for a set 𝒜 consisting of {α, β, γ}, 𝒫(𝒜) = {∅, {α}, {β}, {γ}, {α, β}, {α, γ}, {β, γ}, {α, β, γ}}.

This definition of power set was used to optimise the naïve implementation. Further optimisations were developed on top of this implementation. Several search heuristics were considered for the improvement of the implementation. The binary search and ternary search was chosen for the optimisation. Several tests were made to compare the performance of these heuristics and these are some of the results:

bst3
bst4

The reasoner was developed using Java, the source code of which can be found at the link below.

GitHub Repository

Knowledge Base Generation

Testsets containing knowledge bases with different features were required for the testing of the Rational Closure and Lexicographic Closure algorithms. To accomodate this, a parameterized knowledge base generator was designed and implemented.

The parameters provided were:

Defeasible Statement Count
The total number of defeasible statements in the knowledge base.
Defeasible Rank Count
The total number of defeasible ranks in the knowledge base.
Defeasible Statement Distribution
The distribution function that defines the distribution of the defeasible statements among the defeasible ranks.
Defeasible Only Generation
Whether or not the knowledge base should contain only defeasible statements or a mixture of defeasible and classical statements.

Since this investigation into the scalability of KLM-style defeasible reasoning algorithms, along with the creation of this tool, is one of the first of its kind, the usefulness of the chosen parameters were investigated as well. This was done through analysing the results of the Rational Closure and Lexicographic Closure testing procedures and identifying which parameters lead to tangible takeaways.

The tool was developed using Scala, the source code of which can be found at the link below.

GitHub Repository

Results and Conclusions

Rational Closure Optimisations Results

The implementation of the binary search optimisation outperformed the naive implementation significantly for cases where the premise of our defeasible claims become consistent with our knowledge base at very high rank numbers. The rank-storing approach yielded impressive results where the statements we were querying our knowledge base with had a large number of repeated premises/antecedents.

Lexicographic Closure Optimisations Results

The implementation of the ternary search optimisation outperformed the implementation of the binary search optimisation for the tests that have been made. The above remains unchanged regardless of the distribution of the knowledge base.

Knowledge Base Generation Results

Each parameter was found useful in the analysis of the Lexicographic Closure and Rational Closure optimisations. For instance, it was found that Lexicographic Closure can process knowledge bases containing defeasible and classical statements faster than a knowledge base containing only defeasible statements but with the same total number of statements and ranks.

Downloads