Limbo: A Reasoning System for Limited Belief

1 Introduction

Reasoning about incomplete knowledge is part and parcel of intelligent behaviour. Unfortunately, it often requires highly expressive languages to accurately represent the incompleteness of knowledge, and this high degree of expressivity typically leads to poor computational complexity. This trade-off is what makes designing languages and systems for Knowledge Representation and Reasoning a notoriously difficult taks.

One approach to deal with the complexity of very expressive languages is through limited belief. Originally motivated by philosophical considerations [Hintikka, 1975], the idea behind limited belief is to weaken the logical entailment relation in a way that preserves soundness but trades completeness for better computational complexity. Despite these appealing properties, limited belief has remained a tool for theoretical analysis without practical relevance until now.

This demo showcases LIMBO, 1 a system for reasoning about limited belief in first-order knowledge bases. LIMBO implements the theory of limited belief from [Schwering, 2017], which itself is based on earlier work by Liu, Lakemeyer, and Levesque [2004; 2013; 2014; 2016]. To my knowledge, LIMBO is the first implementation of any of these theories.

This demo aims to show that (i) limited belief is not just a theory but also has practical value and that (ii) LIMBO makes a useful framework for bringing to "life" otherwise predominantly theoretical work such as theories of actions, belief change, and multi-agent reasoning.

1 The following material is available online:

Source code: www.github.com/schwering/limbo Examples: www.cse.unsw.edu.au/~cschwering/limbo Video: www.cse.unsw.edu.au/~cschwering/limbo/video

1 Sort HUMAN, BOOL 2 Name Frank, Fred, Sally -> HUMAN 3 Name T -> BOOL 4 Fun fatherOf/1 -> HUMAN 5 Fun rich/1 -> BOOL 6 Var x -> HUMAN 7 // Sally's father is Frank or Fred, and he's rich. 8 KB: fatherOf(Sally) = Frank v 9 fatherOf(Sally) = Fred 10 KB: rich(fatherOf(Sally)) = T 11 // Is Sally's father rich but unknown? 12 K<1> ex x (fatherOf(Sally) = x ˆ rich(x) = T ˆ M<1> fatherOf(Sally) /= x)

Listing 1: A simple reasoning problem specified in LIMBO's textual interface. Lines 1-6 declare non-logical symbols; lines 8-10 define the knowledge base; line 12 specifies a query.

2 The Reasoning System

The representation language of LIMBO is a first-order modal dialect with functions, equality, sorts, and introspective belief operators [Schwering, 2017]. Semantically, belief is stratified in levels: level 0 comprises only the explicit beliefs; every following level draws additional inferences by doing another case split. Every belief operator specifies at which belief level it shall be evaluated, and thus controls how much effort should be spent on proving it.

Let us illustrate LIMBO's expressivity with a brief example. Suppose that all we know is that either Frank or Fred is Sally's father and that Sally's father is rich. Intuitively this knowledge base should entail the query "we don't know Sally's father, but we do know he's rich." Formalising this query however is not trivial at all, as it requires a significant degree of expressivity: it involves an individual (Sally's father) and both knowns (he's rich) and unknowns (his identity) about him.

First-order modal logic provides a way to express the above knowledge base and query. A formalisation in the language of LIMBO's textual user interface is given in Listing 1. In the following we describe what LIMBO by means of this example.

Names in LIMBO represent distinct objects. For instance, Frank, Fred, and Sally represent three different individuals of the same sort HUMAN. LIMBO assumes for every sort the existence of an infinite number of such objects. In logical terminology, Names are constants that satisfy the unique-name assumption and an infinitary version of domain closure.

Aside from these special constants, LIMBO also supports classical functions, such as the unary function fatherOf that returns an object of sort HUMAN. Predicates are not part of the language at the moment; they can however easily be simulated without overhead with functions of a special sort and a distinguished name that represents truth, such as Bool and T.

Knowledge bases in LIMBO are subject to two syntactic restrictions: they must be in clausal form and contain no existential quantifiers. The former however is no effective restriction as existentials can be simulated with Skolem functions. The semantic concept underlying a knowledge base is Levesque's only-knowing [1984], which implicitly specifies that everything that is not entailed by the knowledge base is unknown.

The query in Listing 1 intuitively says that "we don't know who Sally's father is, but we do know he's rich." The K<1> and M<1> modal operators express what is known and what is considered possible, respectively, at belief level 1. Observe that the variable x is existentially quantified into the modal context of M<1>, which captures the difference between knowing who and knowing that. LIMBO proves the query by splitting the cases for fatherOf(Sally). As for K<1>, if Frank is the father, then he's rich, and if Fred is the father, then he is rich, and every other potential father is ruled out by the knowledge base. As for M<1>, both Frank and Fred are consistent options for fatherOf(Sally), so the father is unknown.

LIMBO is implemented in C++ and closely follows its logical specification [Schwering, 2017]. A noteworthy point about the implementation is that terms and literals have a very lightweight representation. Using a technique called interning, each literal is represented by a single 64-bit number, and whether two ground literals are complementary or one subsumes the other can be computed by bitwise operations on these numbers. This lightweight representation turned out to be 24× faster than the naive representation and helps us to adopt SAT solving technology, where literals by nature are very lightweight. Some syntactic restrictions were useful to facilitate this representation. For instance, we disallow nested functions, so rich(fatherOf(Sally)) = T is flattened to fa x (fatherOf(Sally) /= x v rich(x) = T). Similarly, functions are only allowed on the left-hand side of literals. LIMBO automatically rewrites formulas to adhere to this syntactic format.

3 Experimental Results

We put to test the concept of limited belief using the games of Sudoku and Minesweeper. 2 While both games do not require much expressivity to be modelled, they are nevertheless interesting applications of limited belief because they are known to be computationally hard - Sudoku on N×N grids is NPcomplete, Minesweeper is co-NP-complete - yet often easily solved by humans.

According to the motivating hypothesis behind limited belief, a small belief level should often suffice to reach humanlevel performance. Indeed we find this hypothesis confirmed for both games. The results for Sudoku in Table 1 show that most 'easy' instances are solved just by unit propagation and that the number of necessary case splits moderately increases for 'medium' and 'hard' games. Significantly higher belief levels are needed to solve games from the "Top 1465" list, a repository of extremely difficult Sudokus. For Minesweeper, Table 2 shows that strong results are achieved at level 1 already, and while belief level 2 increases the chance of winning by 0.5%, there is no further improvement at level 3.

4 Discussion and Perspectives

The experimental results show that limited belief is an effective method for bringing first-order epistemic languages to practice. One goal of LIMBO is to encourage authors of related theories in the field of epistemic reasoning to bring their theories to "life" as well. For instance, a theory of (limited) conditional belief [Schwering and Lakemeyer, 2016] has been integrated into LIMBO already. Theories of action [Reiter, 2001; Lakemeyer and Levesque, 2014], belief change [Schwering et al., 2015], and/or multiple agents [Belle and Lakemeyer, 2015] are further candidates to be incorporated.

While the system at the current stage is still a long way from real-world applications, LIMBO's runtime performance appears promising enough to expect useful results from such a highly expressive system; especially considering that SAT solving techniques like clause learning or backjumping are not used by the system yet. With added expressivity, we see potential applications of LIMBO in domains like epistemic planning or high-level control in cognitive robotics.

2 For details on these games, see en.wikipedia.org/wiki/Sudoku and en.wikipedia.org/wiki/Minesweeper (video game).