diff --git a/README.md b/README.md index c54a2d413d440dbf9ebb8b6655b96dc469f93af8..119a0eb9d64c5c53a282052235a6666fb58b645b 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ Limbo is a *reasoning system for a first-order logic of **lim**ited **b**elief*. Limited belief allows for decidable reasoning in first-order knowledge bases, and in the propositional case it is even tractable. See -[\[1,2,3,4\]](#references) for details on the theory, or click +[\[1,2,3,4,5\]](#references) for details on the theory, or click [here](http://www.cse.unsw.edu.au/~cschwering/limbo/) to see some web demos. ## Features @@ -70,18 +70,43 @@ For more theoretical background see the papers linked below. * Improve grounding. * Have a look at some other KR concepts. +## 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: + +```shell +$ git submodule init +$ git submodule update +$ cmake . +$ make +$ make test +``` + ## References -1. Lakemeyer and Levesque. Decidable Reasoning in a Logic of Limited Belief - with Function Symbols. KR 2016. +1. C. Schwering. + A Reasoning System for a First-Order Logic of Limited Belief. + In Proc. IJCAI 2017 (to appear). + [PDF](http://www.cse.unsw.edu.au/~cschwering/ijcai-2017.pdf), + [slides](http://www.cse.unsw.edu.au/~cschwering/ijcai-2017-slides.pdf) +2. G. Lakemeyer and H. Levesque. + Decidable Reasoning in a Logic of Limited Belief with Function Symbols. + In Proc. KR 2016. [PDF](https://kbsg.rwth-aachen.de/sites/kbsg/files/LakemeyerLevesque2016.pdf) -2. Schwering and Lakemeyer. Decidable Reasoning in a First-Order Logic of - Limited Conditional Belief. ECAI 2016. - [PDF](https://kbsg.rwth-aachen.de/sites/kbsg/files/SchweringLakemeyer2016.pdf) -3. Lakemeyer and Levesque. Decidable Reasoning in a Fragment of the Epistemic - Situation Calculus. KR 2014. +3. C. Schwering and G. Lakemeyer. + Decidable Reasoning in a First-Order Logic of Limited Conditional Belief. + In Proc. ECAI 2016. + [PDF](http://www.cse.unsw.edu.au/~cschwering/ecai-2016.pdf), + [slides](http://www.cse.unsw.edu.au/~cschwering/ecai-2016-slides.pdf) +4. G. Lakemeyer and H. Levesque. + Decidable Reasoning in a Fragment of the Epistemic Situation Calculus. + In Proc. KR 2014. [PDF](https://pdfs.semanticscholar.org/8ac9/a2955895cd391ec2b62d8210ee8206979f4a.pdf) -4. Lakemeyer and Levesque. Decidable Reasoning in a Logic of Limited Belief - with Introspection and Unknown Individuals. IJCAI 2013. +5. G. Lakemeyer and H. Levesque. + Decidable Reasoning in a Logic of Limited Belief with Introspection and Unknown Individuals. + In Proc. IJCAI 2013. [PDF](https://pdfs.semanticscholar.org/387c/951016c68aaf8ce36bb87e5ea4d1ef42405d.pdf) diff --git a/examples/tui/test-qbf-1.limbo b/examples/tui/test-qbf-1.limbo new file mode 100644 index 0000000000000000000000000000000000000000..2e54d89f1825722d8891e68ff4705a553a249472 --- /dev/null +++ b/examples/tui/test-qbf-1.limbo @@ -0,0 +1,39 @@ +// ex(x1,fa(x2,ex(x3,fa(x4, (x1 v x2)^ (~x2 v x3)^ (x1 v ~x3))))) +Sort Bool +Name T, X -> Bool +Fun x1/0, x1'/0 -> Bool +Fun x3/0, x3'/0 -> Bool +Fun x2/0 -> Bool +Fun x4/0 -> Bool +Fun sorted/0, pass/0 -> Bool +Fun u0/0, u1/0, y1/0, u2/0, y2/0, u3/0, y3/0, u4/0, y4/0 -> Bool +KB: u0=T +KB: u0=T ^ x1/=X -> u1=T +KB: u0=T ^ ~x1/=X ^ ~y2/=X -> sorted=T +KB: u0=T ^ ~x1/=X ^ ~y3/=X -> sorted=T +KB: u0=T ^ ~x1/=X ^ ~y4/=X -> sorted=T +KB: u0=T ^ ~x1/=X ^ y2/=X ^ y3/=X ^ y4/=X -> sorted=T +KB: u0=T ^ x1'/=X -> u1=T +KB: u0=T ^ ~x1'/=X ^ ~y2/=X -> sorted=T +KB: u0=T ^ ~x1'/=X ^ ~y3/=X -> sorted=T +KB: u0=T ^ ~x1'/=X ^ ~y4/=X -> sorted=T +KB: u0=T ^ ~x1'/=X ^ y2/=X ^ y3/=X ^ y4/=X -> sorted=T +KB: ~x1=T -> pass=T +KB: ~x1'=T -> pass=T +KB: u1=T ^ x2/=X -> u2=T +KB: u1=T ^ ~x2/=X ^ ~y3/=X -> sorted=T +KB: u1=T ^ ~x2/=X ^ ~y4/=X -> sorted=T +KB: u1=T ^ ~x2/=X ^ y3/=X ^ y4/=X -> sorted=T +KB: u2=T ^ x3/=X -> u3=T +KB: u2=T ^ ~x3/=X ^ ~y4/=X -> sorted=T +KB: u2=T ^ ~x3/=X ^ y4/=X -> sorted=T +KB: u2=T ^ x3'/=X -> u3=T +KB: u2=T ^ ~x3'/=X ^ ~y4/=X -> sorted=T +KB: u2=T ^ ~x3'/=X ^ y4/=X -> sorted=T +KB: ~x3=T -> pass=T +KB: ~x3'=T -> pass=T +KB: u3=T ^ x4/=X -> u4=T +KB: u3=T ^ ~x4/=X -> sorted=T +KB: u4=T -> sorted=T +Assert: K<4> (sorted=T ^ (~pass=T -> ((x1=T v x2=T)^ (~x2=T v x3=T)^ (x1=T v x3'=T)))) + diff --git a/examples/tui/test-qbf-2.limbo b/examples/tui/test-qbf-2.limbo new file mode 100644 index 0000000000000000000000000000000000000000..4df304dec59d8fbeb7516f7ad835c8150fa85b5a --- /dev/null +++ b/examples/tui/test-qbf-2.limbo @@ -0,0 +1,39 @@ +// ex(x1,fa(x2,ex(x3,fa(x4, (x1 v x2)^ (~x2 v x3)^ (x1 v ~x3)^ (x2 v ~x4))))) +Sort Bool +Name T, X -> Bool +Fun x1/0, x1'/0 -> Bool +Fun x3/0, x3'/0 -> Bool +Fun x2/0 -> Bool +Fun x4/0 -> Bool +Fun sorted/0, pass/0 -> Bool +Fun u0/0, u1/0, y1/0, u2/0, y2/0, u3/0, y3/0, u4/0, y4/0 -> Bool +KB: u0=T +KB: u0=T ^ x1/=X -> u1=T +KB: u0=T ^ ~x1/=X ^ ~y2/=X -> sorted=T +KB: u0=T ^ ~x1/=X ^ ~y3/=X -> sorted=T +KB: u0=T ^ ~x1/=X ^ ~y4/=X -> sorted=T +KB: u0=T ^ ~x1/=X ^ y2/=X ^ y3/=X ^ y4/=X -> sorted=T +KB: u0=T ^ x1'/=X -> u1=T +KB: u0=T ^ ~x1'/=X ^ ~y2/=X -> sorted=T +KB: u0=T ^ ~x1'/=X ^ ~y3/=X -> sorted=T +KB: u0=T ^ ~x1'/=X ^ ~y4/=X -> sorted=T +KB: u0=T ^ ~x1'/=X ^ y2/=X ^ y3/=X ^ y4/=X -> sorted=T +KB: ~x1=T -> pass=T +KB: ~x1'=T -> pass=T +KB: u1=T ^ x2/=X -> u2=T +KB: u1=T ^ ~x2/=X ^ ~y3/=X -> sorted=T +KB: u1=T ^ ~x2/=X ^ ~y4/=X -> sorted=T +KB: u1=T ^ ~x2/=X ^ y3/=X ^ y4/=X -> sorted=T +KB: u2=T ^ x3/=X -> u3=T +KB: u2=T ^ ~x3/=X ^ ~y4/=X -> sorted=T +KB: u2=T ^ ~x3/=X ^ y4/=X -> sorted=T +KB: u2=T ^ x3'/=X -> u3=T +KB: u2=T ^ ~x3'/=X ^ ~y4/=X -> sorted=T +KB: u2=T ^ ~x3'/=X ^ y4/=X -> sorted=T +KB: ~x3=T -> pass=T +KB: ~x3'=T -> pass=T +KB: u3=T ^ x4/=X -> u4=T +KB: u3=T ^ ~x4/=X -> sorted=T +KB: u4=T -> sorted=T +Refute: K<4> (sorted=T ^ (~pass=T -> ((x1=T v x2=T)^ (~x2=T v x3=T)^ (x1=T v x3'=T)^ (x2=T v ~x4=T)))) + diff --git a/src/limbo/format/pdl/parser.h b/src/limbo/format/pdl/parser.h index 3e6dce705d446cf9610c6e7e3ca8ebdfd427ef70..5799181442e08c3c829a442c388a0a5b32ddeeb6 100644 --- a/src/limbo/format/pdl/parser.h +++ b/src/limbo/format/pdl/parser.h @@ -631,7 +631,7 @@ class Parser { return alpha; } - // implication_formula --> disjunctive_formula -> disjunctive_formula + // implication_formula --> disjunctive_formula -> implication_formula // | disjunctive_formula Result> implication_formula() { Result> alpha = disjunctive_formula(); @@ -640,7 +640,7 @@ class Parser { } if (Is(Tok(), Token::kRArrow)) { Advance(); - Result> beta = disjunctive_formula(); + Result> beta = implication_formula(); if (!beta) { return Error>(LIMBO_MSG("Expected right argument disjunctive formula"), beta); }