ratp
ratp is an interactive prover for a variant of propositional linear logic. It is
highly experimental although the code is well-structured and designed to be
easily extended. It is available under the license "Do whatever you want with it".
ratp implements the (simplified) logical consequence judgment of
the paper Separation Logic Contracts for a Java-like Language with Fork/Join (it was
used to prove some examples of this paper). The calculus implemented is
a sequent calculus for propositional linear logic with the following differences:
- It allows weakening.
- It does not feature the '?' exponential.
- It uses notations from java and separation logic (i.e. * instead of the tensor, -* instead of the
lollypop -o, | instead of the external choice, there is no "par" and no negation).
- Axioms for 0, 1, top and bottom are replaced by rules for 'true' and 'false'.
Download:
ratp-0.0.3.tgz
This file contains the following:
- A single jar file to use ratp: bin/ratp-0.0.3.jar
- A description of the calculus implemented: doc/rules.pdf
- The source code: src/ratp/ (note that, to compile ratp, you need at least antlr version 3.0.1)
- Examples of proofs in tests/*.expected
To launch the tool (Java 1.6 or higher recommended (altough not tested, it should work with 1.5)):
java -jar bin/ratp-0.0.3.jar
Here is a sample interaction with the tool:
Welcome to ratp version 0.0.3
Enter '?.' for available commands.
# Proof !(A -* B), A, A |- (B * B).
1: !(A -* B)
2: A
3: A
============
B * B
< contraction ! 1.
1: !(A -* B)
2: !(A -* B)
3: A
4: A
============
B * B
< left ! 1.
1: A -* B
2: !(A -* B)
3: A
4: A
============
B * B
< left ! 2.
1: A -* B
2: A -* B
3: A
4: A
=========
B * B
< consume 3 with 1.
1: A -* B
2: A
3: B
=========
B * B
< consume 2 with 1.
1: B
2: B
====
B * B
< right * 1 0; ax 1; ax 1.
Proof completed!
 (main page)
|
|
Last modification: September 19, 2008
|