JTabWb is a Java framework for developing provers based on terminating sequent or tableau calculi. It provides a generic engine which performs proof-search driven by a user-defined specification. The user is required to define the components of a prover by implementing suitable Java interfaces. The implemented provers can be used as standalone applications or embedded in other Java applications. The framework also supports proof-trace generation, LATEX rendering of proofs and counter-model generation.
Introduction
JTabWb is a Java framework for developing provers based on terminating
sequent or tableau calculi. The project originated as a tool for experimenting and
comparing on the same ground di↵erent calculi and proof-search strategies for
intuitionistic propositional logic. Now it is an advanced general framework which
can be used to implement di↵erent logics and calculi. It can be used either to
implement provers as stand-alone Java applications or as APIs to be integrated
in other Java applications. Di↵erently from other frameworks like [
R 1| . . . | n Clash-detection rule A function associating with any node-set a value in {SUCCESS, FAILURE} Branch-exists rule
R 1 . . . n Meta-backtrack rule A function associating with a node-set an enumeration of rule instances
AbstractFormula
String format()
String format() Strategy Prover Engine RegularRule Strategy getStrategy() Engine( Prover, AbstractNodeSet) ProofSearchResult searchProof() String name() int numberOfConclusions() AbstractFormula mainFormula()
Iterator< AbstractNodeSet> iterator() ClashDetectionRule ProofSearchResult checkStatus()
AbstractNodeSet premise() BranchExistsRule int numberOfBranchExistsConclusions() AbstractFormula mainFormula()
Iterator< AbstractNodeSet> iterator() MetaBacktrackRule AbstractNodeSet premise() int totalNumberOfRules()
Iterator< AbstractRule> iterator()
Basic notions and their implementation JTabWb provides a generic engine that searches for a proof of a goal driven by a user-defined prover. In particular the engine searches for a proof of the goal visiting the proof-search space in a depth-first fashion; at any step of the search, the engine asks to the strategy component of the prover the next rule to apply. The user defines the prover by implementing the interfaces modeling the logical components of the proof-search procedure in Fig. 1. For every component we indicate the corresponding interface and its main methods.
Formulas are the basic elements of the formal system at hand; one can define formulas of any kind, e.g., propositional, first-order or modal formulas, but also “formulas with a sign” or “labelled formulas”. The data structure storing formulas during proof-search is modeled by a node-set. E.g., in the case of a sequent calculus, node-sets represent sequents [ ) ] where and are finite sets or multisets of formulas. Formulas and node-sets only require the implementation of a method format(), which is invoked by the engine to print detailed information about the proof-search process.
JTabWb models four kinds of rules: regular, clash-detection, branch-exists and meta-backtrack. Regular and clash-detection rules directly correspond to the rules of a calculus; branch-exists and meta-backtrack rules are meta-rules to encode the proof-search strategy. All the rules have AbstractRule as a common supertype.
Regular rules directly correspond to the usual formalization of rules in tableau calculi. A regular rule has the form displayed in Fig. 1: R is the name of the rule, is the premise of R and 1, . . . , n (n 1) its conclusions. We use a double line to represent rules of the framework so to distinguish them from the rules of the sequent calculus we use in the examples.
A rule Rs of a sequent calculus can be mapped to a regular rule R writing
Rs bottom-up (the conclusion of Rs becomes the premise of R). As an example,
let us consider the rule for left disjunction of G3i [
H] [A _ B, [A _ B,
) H] | [B, [B,
H] H] H] )
_ L
H] _ L ) ) The main formula of a regular rule is the formula put in evidence in the premise of the rule (e.g., A _ B in the above example). An instance of a regular rule is an object implementing the RegularRule interface. Conclusions of a regular rule are returned as an enumeration of objects of type AbstractNodeSet. To represent an enumeration of objects we use the Java Iterator interface: it defines the method next() to get the next element in the enumeration and the method hasNext() to check whether the enumeration contains more elements or not.
Clash-detection rules model rules without conclusions corresponding to the end-points of a derivation (closure rules of tableau calculi and axiom rules of sequent calculi). We represent such a rule by a function CD that, given a nodeset , returns SUCCESS if is an end-point of the derivation, FAILURE otherwise. As an example, the axiom rules of G3i
A] [? , )
H] L? correspond to the following clash-detection rule:
CD([ )
A]) =
SUCCESS if ? 2 FAILURE otherwise or A 2 An instance of a clash-detection rule is an object that implements the interface ClashDetectionRule providing the checkStatus() method encoding the corresponding CD function.
The distinction between invertible and non-invertible1 rules has a crucial role
in the definition of a proof-search procedure, since non-invertible rules introduce
backtrack points in proof-search. E.g., the rules of G3i for right disjunction
1 We adopt the formalization of invertible rule of [
LinkedList < Sequent > list = new LinkedList < Sequent >(); Formula [] disjuncts = or_formula . getSubformulas (); for ( int i =0 ; i < disjuncts . length ; i ++){
Sequent conclusion = premise . clone (); conclusion . removeRight ( or_formula ); conclusion . addRight ( disjuncts [i ]); list . add ( conclusion ); } return list . iterator (); } } are not invertible. Indeed, it could be the case that [ ) A2] is provable while [ ) A1] is not. Hence, searching for a proof of [ ) A1 _ A2], we have to try both the rules; if the construction of a proof for [ ) A1] fails, we have to reconsider the premise (backtrack ) and try the other way. The two rules above can be formalized in our framework by means of a branch-exists rule. A branchexists rule R with premise and conclusions 1, . . . , n (n 1) means that is provable i↵ at least one of the i is provable. An instance of a branchexists rule is an object implementing the BranchExistsRule interface. The iterator method returns the conclusions of the rule as an enumeration of objects of type AbstracNodeSet. As an example, in Fig. 2 we describe an implementation of the rules _ Ri of G3i.
A calculus C is a finite set of regular rules, clash-detection rules and branchexists rules. A C-tree ⇡ is a tree of node-sets such that, if is a node of ⇡ with 1, . . . , n as children, then either there exists a regular-rule of C having as premise and 1, . . . , n as conclusions, or n = 1 and there exists a branch-exists rule of C having as premise and 1 as one of its conclusions. A C-proof is a C-tree ⇡ such that, for every leaf of ⇡ , there exists a clash-detection rule CD of C such that CD( ) = SUCCESS.
To define proof-search strategies we need to encode another kind of backtracking arising from the application of non-invertible rules. Let us consider the non-invertible rule ! L of G3i
H] ! L If we are searching for a proof of a sequent containing more than one implication in the left-hand side, we must try all the possible instances of the rule ! L to assert the provability status of . To express this situation we use a meta-backtrack rule, which is a function MB associating with a node-set an enumeration of rule instances having as premise (the non-invertible rules applicable to ). We remark that a meta-backtrack rule is not a rule of the calculus but a meta-rule to encode the proof-search strategy in presence of non-invertible rules.
The strategy is a function that, taken the current goal of the proof-search (a
node-set) and the current state, returns the next rule to apply in the proof-search.
The method nextRule( AbstractNodeSet goal,IterationInfo info) of the Strategy
interface is a callback method invoked by the engine when it needs to determine the
next rule to apply in the proof-search. The engine invokes this method providing
as arguments the current goal of the proof-search and a bunch of data describing
the last move performed by the engine. E.g., the method getAppliedRule() of
IterationInfo returns the rule applied by the engine in the last move; in many cases
this is the only data needed to choose the next rule to apply to goal. For instance,
this is an high-level description of the strategy for a terminating sequent calculus
for intuitionistic propositional logic (as, e.g., the calculus LSJ described in [
IterationInfo info ) { if ( an invertible rule r is applicable to sequent ) return r; } _AbstractRule lastAppliedRule = info . getAppliedRule (); if ( lastAppliedRule is not a clash - detection rule ) return the clash - detection rule for sequent ; if ( non invertible rules r1 ... rN are applicable to sequent ) return the meta - backtrack rule collecting r1 ... rN return null A prover is an object implementing the Prover interface which provides the getStrategy() method and some other methods that are not essential to our discussion. 3
High-level description of the engine We give in Fig. 3 an high-level description of the algorithm implemented by the engine to perform proof-search. An instance of the engine is built by specifying the prover and the goal; searchProof() searches for a proof of the goal driven by the strategy specified by the prover. To simplify the presentation we assume that the data passed to the strategy only consist of the rule applied in the last step. The search space is visited in a depth-first fashion using a stack to store the information related to branch points and backtrack points. More precisely, the stack contains elements (rule,iterator), where rule is the rule that caused the push action, iterator is the associated enumeration. If rule is a regular rule, the element of the stack represents a branch point, if rule is a branch-exists or a meta-backtrack rule, the element represents a backtrack point.
The method searchProof() essentially consists of a loop; we call iteration of the engine an iteration of such a loop. At every iteration the state of the engine is characterized by the current goal of the proof-search (i.e., current goal), the rule to apply in the current iteration (i.e., current rule) and the rule selected for the next iteration (i.e., next rule). If current rule is a regular rule or a branchexists rule, the engine replaces the goal with the first conclusion of the rule and determines the next rule to apply by invoking the strategy. If the applied rule has more than one conclusion, then an element e is pushed on the stack by the call push(current rule,iterator): if current rule is a regular rule, e is a branch point, otherwise e is a backtrack point.
If current rule is a meta-backtrack rule, the associated enumeration iterator collects the rules to be applied to current goal. The first rule in the enumeration (returned by the method next()) is applied and, if iterator contains one or more rules, the backtrack point (current rule, iterator) is pushed on the stack.
If current rule is a clash-detection rule, then the engine invokes checkStatus() to determine if the current goal is an end-point of the proof-search. If checkStatus() returns FAILURE, then the strategy selects the next rule to apply. If it returns SUCCESS, then restoreBranchPoint() searches the stack for a branch point. If such a point exists, it provides the new goal and the strategy selects the next rule to be applied; if the stack does not contain any branch point, the proof-search successfully terminates. The method restoreBranchPoint() searches the stack for a branch point, namely an element (rule,iterator), where rule is a regular rule. If such an element does not exist, it returns null; otherwise, it returns iterator.next(), representing the new goal to be proved. If iterator is empty, the branch point is removed.
If current rule is null, it means that the strategy failed to select a rule for current goal in the last iteration of the engine, hence the proof-search for current goal has failed. In this case the engine searches the stack for a backtrack point invoking restoreBacktrackPoint(). If a backtrack point exists, the engine appropriately updates its state and starts a new iteration. Otherwise, it returns FAILURE to signal that a proof for the input goal does not exist. The method restoreBacktrackPoint() searches the stack for a backtrack point, that is an element (rule,iterator), where rule is a branch-exists rule or a meta-backtrack rule. If such an element does not exist, null is returned; otherwise, the pair (rule,iterator.next()) is returned. In the latter case, if rule is a branch-exists rule, then iterator.next() is a node-set (the next goal to be proved); otherwise, rule is a meta-backtrack rule and iterator.next() is the next rule to be applied. // goal and prover are the arguments of the engine constructor current goal = goal strategy = prover.getStrategy() next rule = strategy.nextRule(current goal,null) while true do current rule = next rule // the only data about the last iteration if current rule is a regular rule then iterator = current rule.iterator() current goal = iterator.next() next rule = strategy.nextRule(current goal,current rule) if iterator.hasNext() then push(current rule,iterator) end else if current rule is a branch-exists rule then iterator = current rule.iterator() current goal = iterator.next() next rule = strategy.nextRule(current goal,current rule) if iterator.hasNext() then push(current rule,iterator) end else if current rule is a clash-detection rule then if current rule.checkStatus() == SUCCESS then current goal = restoreBranchPoint() // restored is a goal or
null if current goal == null then return SUCCESS else next rule = strategy.nextRule(current goal,null) end else next rule = strategy.nextRule(current goal,current rule) end else if current rule is a meta-backtrack rule then iterator = current rule.iterator() next rule = iterator.next() if iterator.hasNext() then push(current rule,iterator) end else if current rule is null then r = restoreBacktrackPoint() // r is a pair if r == null then return FAILURE if snd(r ) is a rule then //rule is a meta-backtrack rule next rule = snd(r ) // snd(r ) is the next rule to try current goal = fst(r ).premise() // restore the goal from the
rule else //rule is a branch-exists rule current goal = snd(r ) // snd(r ) is the next sub-goal to try next rule = strategy.nextRule(current goal,current rule) end end end
52 4
Implemented provers and other features The engine can be executed in verbose mode to get a detailed description of the proof-search or in trace-mode to generate a trace of the proof-search. It is possible to generate the LATEX rendering of the C-trees visited during the proof-search (this only requires to provide the data rendering for node-sets and rule names). The trace of a proof-search can be used to generate the countermodel for unprovable goals. JTabWb also provides some useful support APIs (jtabwbx.* packages): two implementations of propositional formulas, a parser for propositional formulas and a command line launcher for a prover.
We have implemented several provers for intuitionistic propositional logic in
the JTabWb framework. g3ibu is a prover based on the sequent calculi Gbu and
Rbu [
As for future work, we are developing a language to specify the components of a JTabWb prover and a library of formulas implementations and node-set implementations that can be used as building blocks for provers. Finally, we remark that the JTabWb can be used also to implement calculi for first-order logic and, in general, non terminating calculi. What is missing for fruitfully use these kind of calculi is a support which allows the user to directly control the engine execution. We are developing it as an interactive version of the engine.