File	Date	Author	Commit
graphView	2011-12-23	fneuhaus	[305015] Merge with 0791cfd5dca72dd73956977b9c2badc64135...
mxgraph	2011-12-23	fneuhaus	[305015] Merge with 0791cfd5dca72dd73956977b9c2badc64135...
priklReasoner.api	2012-02-09	stixier	[dfb4a4] Proof update
priklReasonerImpl	2012-04-13	stixier	[5b500c] Fix tests
.hgignore	2012-01-27	fneuhaus	[39e26e] Merge with a2b1c64e3861107c45f794aa65213b6f0adc...
README.txt	2011-12-07	stixier	[859545] Merge with 0e07b12a217ebbe4df82c76c410329257614...
pom.xml	2011-12-23	fneuhaus	[305015] Merge with 0791cfd5dca72dd73956977b9c2badc64135...

Read Me

This is the README for PrIKL, a reasoner currently developed by the
National Institute of Standards and Technology.  The reasoner uses a
hybrid of a natural deduction system and a production system.  For an
overview of PrIKL, please read the Overview paper currently in
preparation.

* Version

This is alpha release version .2.0.  The first production release will
be called 1.0.

* Contact

There are several Prikl-related mail lists accessible from PrIKL's
sourceforge page.

prikl-announcements: PrIKL-related announcements.

prikl-administration: Prikl-related administrative issues such as
access to the code, problems with the mail list, etc.

prikl-developers: Discussion between PrIKL developers.

Please do *not* send bug reports to these lists unless there is a good
reason why you aren't following the Bug Reporting procedures described
elsewhere.)

* Sourceforge

Currently, we use a repository internal to NIST for primary
development.  However, we do frequently push updates to our public
repository on sourceforge.  In addition, we encourage public
developers to use the sourceforge repository.  We are using mercurial
to do version control so we can integrate bug fixes from sourceforge.

Our sourceforge repository is:

http://sourceforge.net/projects/prikl/

Write access to the sourceforge repository must be preapproved by the
current developers.  If you would like to contribute, please use the
prikl-administration mail list mentioned elsewhere.

* Bug Reporting

The best way to report bugs is to use the bug reporting mechanism at
sourceforge.

* Typography

The official spelling of PrIKL is with lowercase 'r'.  The spelling in
the code or when launching it from the command-line is 'prikl' in all
lower-case.  We will not flinch if you spell it without the unusual
case.  However, if you add an 'e' at the end, you will confuse
everyone!

* To install

PrIKL is currently runnable in two ways:
- Executable JAR: This offers a built-in GUI for simple experiments.
- Source: Using the source gives the full power of PrIKL.

Executable JAR

To run a jar on a system where you can click on it, try clicking.  If
clicking or double-clicking on it.  If that doesn't work, read:

http://www.wikihow.com/Run-a-.Jar-Java-File

To run a jar from the command line, enter:

% java -jar name-of-jarfile.jar

where "%" is your command prompt and "name-of-jarfile.jar" is the
jarfile.

If this doesn't work, ask a local java expert.

Source

There are a variety of ways to run from the source.  Anyone doing this
is presumed to need less handholding.

We run the source within an IDE (Interactive Development Environment)
and use both Eclipse and Netbeans.  We do most of our development
within Eclipse while we do our GUI development within Netbeans.

Tests

The test directory has many tests.  Unfortunately, last minute changes
have broken some of them so running all of them is not a useful way of
testing that the system is working.  Nonetheless, a lot of the tests
show some of the interesting aspects of PrIKL and are worth trying or
at least looking at.

* Configuration

Most of the configuration options have been isolated to the file:

src/main/resources/prikl_config.properties

Most of the options in the properties file controls debugging output.
However, there are a few options that are worth mentioning.

* Limitations

This release is known to have bugs and there are many missing
features.  Feel free to browse the bug tracker at sourceforge.  A few
notable issues are mentioned here:

Decision Procedure

The current decision procedure implementation has been found to be too
inefficient and we plan to replace it.  Do not enable the decision
procedure at this time.

Plugins

The 'equal' plugin is required for sentences using identity (=).
However, the other plugins are optional.  You can disable them but
there is essentially no burden placed on the system leaving them
enabled.  However, there is currently no namespacing so you may run
into conflicts if you use a name already used by one of the plugs.
For example, if you the string plugin and use the concat in a
predicate position, the system will use the string plugin to do
concatenation on the remaining arguments.

Split Size

The system currently uses Java's built-in serialization when splitting
a problem.  We recently discovered that Java serialization makes
excessive use of the stack.  Therefore, if your problem splits, you
either must limit the size of your problem (we found stack overflows
in problems with about 5000 assumptions) or you must increase Java's
default stack size.  We are looking addressing this problem with an
alternate implementation.

Identity 

Support for identity is incomplete.  More word to come on this.