B I L L: A theorem prover for propositional BI logic

Frédéric Béal, Daniel Méry and Didier Galmiche (TYPES, LORIA UMR 7503)

Description

BILL is an automated theorem prover for the propositional fragment of BI, the Logic of Bunched Implications,
introduced by D.J. Pym and P.W. O'Hearn in 1999. This new resource-aware logic can be viewed as a
well-founded merging of intuitionistic logic IL and multiplicative intuitionistic linear logic MILL.
Its semantics and proof theory are defined in [1,2].

BILL is an implementation of a new tableau method for BI that is based on labels and label constraints.
Its proof-theoretic foundations are presented in [3,5] where one only deals with propositional BI logic
without bottom. A similar method has been proposed in [4] for BI (including bottom) with decidability
and finite model property has main consequences.
As BI is conservative over both IL and MILL, BILL also provides new theorem provers for both logics,
that are based on labels and constraints.

The first version of BILL was mainly written in OCaml by Frédéric Béal during its post-master degree
training period. This version only deals with propositional BI without the units (bottom, top and I).
New versions including extensions to units (mainly bottom), improvements and optimisations,
are under development.

References

[1] P.W. O'Hearn and D.J. Pym The Logic of Bunched Implications.
Bulletin of Symbolic Logic, vol. 5, no 2, pp 215-244, 1999.

[2] D.J. Pym The Semantics and Proof Theory of the Logic of Bunched Implications.
Applied Logic Series, vol. 26, Kluwer Academic Publishers, 2002.

[3] D. Galmiche and D. Méry Proof-search and Countermodel Generation in Propositional BI Logic.
International Symposium on Theoretical Aspects of Computer Software, TACS 2001,
Tohoku University, Sendai, Japan, October 2001.

[4] D. Galmiche, D. Méry and D. Pym Resource Tableaux (extended abstract).
Int. Conference on Computer Science Logic, CSL'02,
Edinburgh, Scotland, September 2002.

[5] D. Galmiche and D. Méry Semantic Labelled Tableaux for propositional BI (without bottom).
To appear in Journal of Logic and Computation, september 2002.

How to get BILL

BILL can be freely downloaded, copied, modified and redistributed under the terms of the GNU Public License, version 2.

You must first download the archive (here) of the sources, then, extract the files and compile them as follows
(you will need OCaml v3.02 or higher):

tar xvzf BILL-1.01b.tar.gz
cd BILL-1.01b
make

Usage

After compiling the sources, you just have to type ./bill in the directory where BILL has been installed.
The prompt BILL> should appear to indicate that the system is ready to interact with you. First try to type
the command help to display a short description of the prover syntax.
For a more detailed explanation on how to use BILL you should read the HELP text file.

A version of BILL has been designed for the particular case of MILL, including specific refinements and optimisations.
This version is obtained by typing ./mill in the directory where BILL has been installed.
Note that this specialized version of the prover does not include the countermodel facility.

Example of a BILL session

 
% ./bill

Propositional BI
Version 1.01
Ctrl+D to quit

BILL> help
Variables: [A-Za-uw-z]
Connectives: -*, *, ->, ^, v 
Precedence: ->, -* < v < ^, *
Commands: 
  help: prints this page
  check <p>: decides proposition <p>
  depth <n>: sets search-depth to <n>
  stat: statistics about proof-search
  tex cm<file>: saves countermodel in a tex file
BILL> check ((a->(b-*c))-*((a->b)-*(a->c)))
false: ((a->(b-*c))-*((a->b)-*(a->c)))
BILL> stat
search-time: 0.000
search-calls: 10
BILL> tex cm-formula-1
countermodel written in tex/cm-formula-1.tex
BILL>