BBeye: A Theorem Prover for Boolean BI (Bunched Implications)

Jeongbong Seo, Jonghyun Park, and Sungwoo Park

Introduction

BBeye is an automated theorem prover for Boolean BI (Bunched Implications), the underlying theory of separation logic. BBeye implements a backward search strategy on top of a nested sequent calculus called S_BBI. Internally BBeye uses another nested sequent calculus CS_BBI in which weakening and contraction are built into all the other rules, and its variant called the labelled CS_BBI. Both CS_BBI and the labelled CS_BBI are equivalent to S_BBI.
Given a goal formula, BBeye first performs proof search in the labelled CS_BBI. Then it converts the proof into a corresponding proof in CS_BBI, which is finally converted into a corresponding proof in S_BBI. BBeye implements a certifier for each of S_BBI, CS_BBI, and the labelled CS_BBI. Thus users only need to trust S_BBI, which is sound and complete with respect to the Kripke semantics of Boolean BI and the Hilbert system.
BBeye is implemented in the style of an interactive theorem prover. It provides an automation tactic auto for performing proof search, as well as a number of tactics for applying inference rules in CS_BBI or the labelled CS_BBI.


Online demo of BBeye


How to install BBeye

Requirements

To install BBeye, you need the following software and libraries: Install GODI with OCaml v3.12.1 or higher. Then use GODI to install Jane Street's Core library, Ocamlgraph library, and LablGTK2 library. Download and install Graphviz. The current release of BBeye compiles with Jane Street's Core library v107.01#5.

Download and install

BBeye is freely available under the terms of the GNU Lesser General Public License Version 2.1. It can be downloaded as a gzip'd tarball [prover.tar.gz]. After downloading, extract the files and compile them as follows:

tar xvzf prover.tar.gz
cd bbeye
make			# for command line interface 
make GUI.native		# for GUI
make Test.native 	# for compiling Test.ml 


Usage

  1. Run ./CUI.native where BBeye has been installed.
    After the status message, the prompt > should appear to indicate that the system is ready to interact with you.
  2. Type open formula to start a new proof session. Type help to see the syntax of formulas.
  3. If you type a valid formula, a new session is created and the goal statement is displayed.
  4. Type auto to solve the goal automatically. BBeye uses an internal parameter, which we call depth, to control the size of search space. The default depth is 2, but you can specify it as an argument to auto, e.g., auto 3. (A depth does not mean the height of a proof tree; it is the number of a special set of inference rules.)
  5. If BBeye succeeds to find a proof, a message is displayed.
  6. Type history to see a brief version of the proof tree. Type savefilename to save the labelled CS_BBI version of the proof tree.
  7. Type close to discard the current session and start another proof session.
For GUI, you can use show all, show visible, and show toggle to change the way that proof trees are displayed. To test BBeye, run make Test.native; ./Test.native. Test.ml contains many interesting test cases for Boolean BI.


Examples of running BBeye

To prove a formula automatically

1. Let us prove a formula 'I/\A->A*A'. Type 'open I/\A->A*A'.
Idle. Type 'open <PROPOSITION>' to start a session. ex) open A->A
--------------------------------------------------------------------------------
> open I/\A->A*A


1 Subgoal(s)
Rooted proof tree is:

Seq #0: w0
  fc= 0:I/\A->A*A

--------------------------------------------------------------------------------
>
2. Type auto to solve the goal automatically.
> auto

Proof completed! Type 'save "filename"' to save the proof to the file "filename".
--------------------------------------------------------------------------------
>
3. Type save "ex1.tex" to save the proof in a latex file.
> save "ex1.tex"
Saved the proof to 'ex1.tex'.

Proof completed! Type 'save "filename"' to save the proof to the file "filename".
--------------------------------------------------------------------------------
>
4. Type close to end the proof session.
> close

Idle. Type 'open ' to start a session. ex) open A->A
--------------------------------------------------------------------------------
>
5. Now, try to prove another formulaA*B*C*D->D*B*C*A.
> open A*B*C*D->D*B*C*A

1 Subgoal(s)
Rooted proof tree is:

Seq #0: w24
  fc= 0:A*B*C*D->D*B*C*A

--------------------------------------------------------------------------------
> auto
auto fails: Cannot find the proof. Try with a deeper depth. ex) auto 3
--------------------------------------------------------------------------------
>
6. The proof search failed with depth 2 (default value). We can prove this formula with search depth 3.
> auto 3

Proof completed! Type 'save "filename"' to save the proof to the file "filename".
--------------------------------------------------------------------------------
> 

To prove a formula manually

1. To prove a formula 'I->(a-*(b->c))-*((a-*b)->(a-*c))', type 'open I->(a-*(b->c))-*((a-*b)->(a-*c))'.
On the left top window, the goal (labelled CS_BBI sequent) is printed. For clarity, we classify and gather the sequent elements according to the node name so that each cluster looks like following:

Seq #[sequent index]:[node name] 
/<Mzero>/
GS= ([index]:[nodename]-[node name])+ 
TC= ([index]:[Proposition])+
FC= ([index]:[Proposition])+
GS, TC, and FC stands for 'Graph Structure', 'Truth Context', and 'Falsehood Context'. We omit each context when it is empty.
On the right window, you can see the visualized sequent.

2. To apply the rule ImplyR with the first falsehood formula (whose index is 0) at node w0 (whose index is 0), type apply ImplyR 0 0.

3. In a similar way, you can apply the rule UnitL with the first truth formula (which is I) at node w0 by typing apply UnitL 0 0.

4. trivial command exaustively applies the rules except the rules 'StarR', 'WandL', 'ZeroU', and 'ZeroD' which explode the search space. To see the result, type history to print the incomplete proof tree.

5. To apply the rule WandL with the first relation and the first truth formula at node w2 (whose index is 3), type apply WandL 3 0 0. It generates two subgoals and focuses on the first one.

6. Apply the rule Init to finish the subgoal (apply Init 0 0 0) or type auto to let the prover solve it.

7. Apply apply Comm 3 0 and apply Assoc 2 4 0 to change the structure of the goal.

8. Notice that it displays only those nodes with high priority (drawn in green). To display all nodes, type show toggle, which shows nodes with low priority as well (drawn in black). To toggle display mode, type the same command again.

9. Type auto to prove the goal automatically.


Email us at .

Programming Language Laboratory
Department of Computer Science and Engineering
Pohang University of Science and Technology (POSTECH)
Republic of Korea