Jeongbong Seo, Jonghyun Park, and Sungwoo Park
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.
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
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 'open5. Now, try to prove another formulaA*B*C*D->D*B*C*A.' to start a session. ex) open A->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". -------------------------------------------------------------------------------- >
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.
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.
Programming Language Laboratory Department of Computer Science and Engineering Pohang University of Science and Technology (POSTECH) Republic of Korea