Limbo is a reasoning system for modelling and querying an agent’s knowledge. Limbo features a highly expressive modelling language (with functions, equality, quantification, introspective modal operators), but maintains attractive computational properties.
Great expressivity usually brings along great computational complexity. Limbo avoids the computational cliff using the theory of limited belief, which offers a principled way to control the computational effort and preserves decidability and, in the propositional case, even tractability.
A quick example of the modelling language: the statement “I know Sally’s father is rich, but I don’t know who he is” can be encoded by the following Limbo formula: K1 exists x (fatherOf(Sally) = x ^ rich(x) = T ^ M1 fatherOf(Sally) /= x). The operators K1 and M1 refer to what the agent knows or considers possible, respectively, at belief level 1; the belief level is the key concept that controls the computational effort.
Limbo is a C++ library. Started as an academic proof of concept, it’ll hopefully develop into a practical reasoning system in the longer run. The name Limbo derives from limited belief with an Australian ‘-o’ suffix.
Where to go from here?
Limbo provides a logical language to represent and reason about (possibly incomplete) knowledge and belief.
This logical language is a first-order modal dialect: it features functions and equality, standard names to designate distinct objects, first-order variables and quantification, sorts, and modal operators for knowledge and conditional belief. (Predicates are not built-in but can be simulated without overhead using boolean functions.)
An agent’s knowledge and beliefs are encoded in this language. This knowledge base is subject to a syntactic restriction: it must be in clausal form, and all variables must be universally quantified; however, as existentially quantified variables can be simulated through Skolemization, this is no effective restriction. An example knowledge base might assume a birthday scenario and stipulate that that a certain gift box is known to contain an (unknown) gift.
Reasoning in such knowledge bases is done with queries expressed in this language. For example, we can say that we believe that something is in the box and that we have no idea what it is. A decision procedure evaluates such queries in a way that is sound but incomplete with respect to classical logic. That is, if the procedure says that the knowledge base entails the query, then this correct, but conversely the procedure may miss some true queries. Completeness is sacrificed for decidability, which means that the procedure actually terminates. (Soundness, completeness, decidability in first-order logic is one of those “pick any two” scenarios.)
How much effort (and time) is spent on evaluating a query is controlled through a parameter that specifies how many case splits the reasoner may investigate. Every modal operator is decorated with such an effort parameter. This effort parameter and its limiting effect on the reasoning capabilities is the key ingredient to achieve decidability without restricting the syntactical expressivity of queries. This sets this theory apart from decidable syntactical subclasses of first-order logic and from description logics.
For more theoretical background see the papers linked below.
Interesting KR concepts to be added include:
To improve the performance, we could investigate:
The library is header-only and has no third-party dependencies. It suffices to
have src/limbo in the include path.
To compile and run the tests and demos, execute the following:
$ git clone https://github.com/schwering/limbo.git
$ cd limbo
$ git submodule init
$ git submodule update
$ cmake .
$ make
$ make test
The first paper is the most recent one and describes the theory behind Limbo. I’m working on a technical report that includes new development since (and fixes a bunch of bugs in the extended version). Many of the ideas were introduced in the earlier papers linked below.