Coder Social home page Coder Social logo

limbo-1's Introduction

A Reasoning System for First-Order Limited Belief

Note: This rewrite branch is far from finished. Check out the master branch for a more stable version. Most of the below text refers to the old version (in particular, the web demos are still running a version from 2017).

Limbo is a reasoning system for modelling and querying an agent's knowledge. Limbo features a highly expressive modelling language that includes functions, equality, quantification, introspective modal operators, but maintains attractive computational properties.

Great expressivity usually brings great computational complexity. Limbo avoids the computational cliff using a 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 that 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: [email protected].

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 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 on-line demos are still based on an earlier version. They'll be updated when the current rewrite is finished.)

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:

  • 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 checkout master # the `rewrite' branch is far from finished
$ git submodule init
$ git submodule update
$ cmake .
$ make
$ make test

References

The papers below describe the theory behind Limbo. They are ordered, roughly, by relevance for Limbo: papers [1, 2] are the ones most closely related to the current state of the implementation, the remaining ones cover other aspects of the theory. I'm working on a technical report that includes all new developments since [1, 2] (and fixes a few bugs in the extended version of [1]).

  1. A Reasoning System for a First-Order Logic of Limited Belief.
    C. Schwering.
    In Proc. IJCAI, 2017.
    pdf, slides
  2. Limbo: A Reasoning System for Limited Belief
    C. Schwering.
    In Proc. IJCAI, 2017.
    pdf
  3. The Complexity of Limited Belief Reasoning โ€” The Quantifier-Free Case
    Y. Chen, A. Saffidine, C. Schwering.
    In Proc. IJCAI, 2018.
    pdf, slides
  4. A Representation Theorem for Reasoning in First-Order Multi-Agent Knowledge Bases
    C. Schwering, M. Pagnucco.
    In Proc. AAMAS, 2019.
    pdf, slides
  5. Reasoning in the Situation Calculus with Limited Belief
    C. Schwering.
    Commonsense, 2017.
    pdf, slides
  6. Decidable Reasoning in a Logic of Limited Belief with Function Symbols.
    G. Lakemeyer and H. Levesque.
    In Proc. KR, 2016.
    pdf
  7. Decidable Reasoning in a First-Order Logic of Limited Conditional Belief.
    C. Schwering and G. Lakemeyer.
    In Proc. ECAI, 2016.
    pdf, slides
  8. Decidable Reasoning in a Fragment of the Epistemic Situation Calculus.
    G. Lakemeyer and H. Levesque.
    In Proc. KR, 2014.
    pdf
  9. Decidable Reasoning in a Logic of Limited Belief with Introspection and Unknown Individuals.
    G. Lakemeyer and H. Levesque.
    In Proc. IJCAI, 2013.
    pdf

limbo-1's People

Contributors

schwering avatar timn avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.