This is a reasoning engine for Complex Epistemic Modalities in the Situation 
Calculus It was developed as part of Ryan Kelly's PhD thesis "Asynchronous 
Multi-Agent Reasoning in the Situation Calculus".  Further details are
available at:

   http://www.rfk.id.au/research/thesis/

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program.  If not, see <http://www.gnu.org/licenses/>.

---------------------------------

To get up and running, you will need a working installation of SWI-Prolog,
available from:

   http://www.swi-prolog.org/

As well as the "twbcompile" program from the Tableaux Workbench Suite:

   http://twb.rsise.anu.edu.au/


---------------------------------

This is a simplistic prolog implementation of epistemic reasoning in the
situation calculus, using techniques from the thesis.  The domain
implemented is the "party invitation" example.
Concurrent actions are not currently supported, although this is purely
an implementation limit.

Fluents are reified for easy manipulation, with the predicate "holds"
evaluating a fluent at a given situation.  Used like so:

    ?- [main].
    true.

    ?- holds(loc(c),s0).
    true.

    ?- holds(knows(ann,loc(C)),s0).
    fail.

    ?- holds(knows(ann,loc(C)),do(read(ann),s0)).
    true.


We assume all variables have a finite domain, so that fluents can be
propositionalized to perform reasoning.  We have modified the PDL
prover from the Tableuax Workbench project do handle variable assignments,
which we shell out to for the actual reasoning.  You will need to compile
the file "vpdl/vpdl.ml" using the TWB compiler; `make` should do this for you.

The included files are:

  * fluent.pl:  Create and manipulate reified fluent terms.  This file also
                provides simplication routines to help keep the size of
                fluent terms manageable.

  * epath.pl:   Create and manipulate epistemic path terms.  This is pretty
                similar in scope to fluent.pl.

  * twb_pdl.pl:  Interface with the PDL prover for the Tableaux Workbench
                 project to static epistemic reasoning.

  * sitcalc.pl:  Domain-independent sitcalc primitives, such as regression()
                 and holds().

  * domain.pl:  Domain-specific predicates, such as ADP fluent definitions,
                causes_true/causes_false, etc.

  * vpdl/*:     Modified PDL prover that can handle variable assignments.


The files come with unit tests included, which may help demonstrate the syntax
and use of the various predicates.  To run the test suite, do the following
in the prolog shell:

    ?- [main].
    ?- run_tests.