A Reasoning System for a First-Order Logic of Limited Belief
C++ CMake
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.

README.md

A Reasoning System for First-Order Limited Belief

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?

  • You could check out the web demos to see limited belief in action.
  • You could check out the code and compile it and run Limbo on your computer.
  • You could have a look at one of the papers on the theory behind Limbo.
  • You could also send me an email: c.schwering@unsw.edu.au.

Features

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.

Examples

  • This web demo allows to define and query a knowledge base through a simple text interface. You can also use it from the command line; the the code is here.
  • There's are Minesweeper and Sudoku web demos. You can use them it from the command line as well; the the code is here and here.
  • The main part of the C++ API is kb.h, formula.h, clause.h, literal.h, term.h, in this order. Optional C++ operator overloadings are provided by format/cpp/syntax.h to make creating formulas a little more convenient.

Future work

Interesting KR concepts to be added include:

  • Progression for actions.
  • Sensing and/or belief revision.
  • Multiple agents.

To improve the performance, we could investigate:

  • Clause learning, including its theoretical implications.
  • Backjumping.
  • More efficient grounding.

Installation

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

References

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.

  1. A Reasoning System for a First-Order Logic of Limited Belief.
    C. Schwering.
    In Proc. IJCAI, 2017.
    pdf, proofs, slides
  2. Limbo: A Reasoning System for Limited Belief
    C. Schwering.
    In Proc. IJCAI, 2017.
    pdf
  3. Reasoning in the Situation Calculus with Limited Belief
    C. Schwering.
    Commonsense, 2017.
    pdf
  4. Decidable Reasoning in a Logic of Limited Belief with Function Symbols.
    G. Lakemeyer and H. Levesque.
    In Proc. KR, 2016.
    pdf
  5. Decidable Reasoning in a First-Order Logic of Limited Conditional Belief.
    C. Schwering and G. Lakemeyer.
    In Proc. ECAI, 2016.
    pdf, slides
  6. Decidable Reasoning in a Fragment of the Epistemic Situation Calculus.
    G. Lakemeyer and H. Levesque.
    In Proc. KR, 2014.
    pdf
  7. Decidable Reasoning in a Logic of Limited Belief with Introspection and Unknown Individuals.
    G. Lakemeyer and H. Levesque.
    In Proc. IJCAI, 2013.
    pdf