# The homepage of the PrInS theorem prover

## What is PrInS?

PrInS is a theorem prover for first order logic. It's main features are
as follows.

- It uses a non-backtracking tableau procedure,
known as incremental closure.
- It uses constrained formula
free-variable tableaux.
- Unlike most other theorem provers, it does not work on clause
normal form, but on negation normal form.
- For enhanced efficiency, it uses a set of simplification rules in a strategy that
amounts to a non-normal form version of hyper tableaux.
- It is implemented in the Java programming language.

If you want to know almost all about it, you can read
my
PhD thesis. If you want to know *all* about, you can download it and
read the source.

## Download

You can download the current version of PrInS here:

PrInS-0.83.tar.gz

Apart from Java, you will need a couple of libraries to compile it:

- The parser generator ANTLR, available
here.
(Tested with v2.7.2)
- The unit testing framework JUnit, available
here.
(Test with v3.8.1)

When you unpack the tar file, you will find two files `README_compile`

and `README_run`

, which might be helpful in getting the thing to work.
If you have trouble, feel free to contact me.

## Known Bugs

PrInS is to be considered in alpha-state. I would not be surprised
if you had trouble compiling it. It has undocumented command line
flags. The output format is not documented either. On some inputs it
just crashes. Also, it occasionally claims to find a proof for
something that is wrong. Please let me know if you find any bugs, though!