Tinybot is a toy implementation of semi-naive bottom up logic programming
Standard ML
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
lib
.gitignore
README.md
Timers.sig
Timers.sml
Timing.sig
Timing.sml
exec-lin.sml
exec-trackdepth.sml
exec.sml
global.sml
index.sml
match.sml
queue.sml
subst.sml
syntax.sml
term-hashcons.sml
term.sig
term.sml
termtable.sml
test-gen.sml
test-lin.sml
test.sml
tinybot-lin.cm
tinybot-simple.cm
tinybot-trackdepth.cm

README.md

tinybot

Tinybot is a toy implementation of semi-naive bottom up logic programming; the several implementations all allow visual stepping through the process of proof search. There are three implementations:

  • tinybot-simple.cm -- Persistent, McAllester-style semi-naive evaluation.

  • tinybot-trackdepth.cm -- Semi-naive evalutation that does some dependency tracking to make sure that each fact is proved with the minimum-depth proof, a change that is important to some algorithms like Meld that do truth management.

  • tinybot-lin.cm -- A very simple example of using the indexing structures from semi-naive evaluation to do linear forward chaining in the style of Ollibot, Lollimon, or Linear Logical Algorithms.

The test/demo/example file test.sml is loaded by all the configuration files; the tests in that file can be run like this:

$ git clone git://github.com/robsimmons/tinybot.git
$ cd tinybot
$ sml -m tinybot-simple.cm # or one of the other two
- Test.test1 ();

The test/demo/example file for linearity test-lin.sml is loaded only by tinybot-lin.cm; it can be run like this:

$ git clone git://github.com/robsimmons/tinybot.git
$ cd tinybot
$ sml -m tinybot-lin.cm
- LinTest.test0 true;