Verbose mode

Running prover X in verbose mode (-v option) we get a detailed description of the performed proof-search. E.g., the following are some steps from the execution of g3ibu in verbose mode on Kreisel-Putnam Principle:

$ java -jar g3ibu-1.0.jar -v wffs/ipl_examples_jtabwb/scott.jtabwb
** Reader [jtawb_format]
> Parsing problem... time (ms) [2]
** Problem [Kreisel-Putnam], status [UNPROVABLE]
> Building initial node set... time (ms) [101]
** Prover [g3ibu 1.0 (seq=bsf, eval=min)]
> Proving...
[0] ------------------------------------ [INITIAL_STATE]
    Stack size [0]
    Initial goal: (0)
    | [U]==>
    | (((p -> false) -> (q | r)) -> (((p -> false) -> q) | ((p -> false) -> r)))
[1] ------------------------------------ [REGULAR_RULE_APPLICATION]
    Stack size [0]
    Selected formula [->-formula]: (((p -> false) -> (q | r)) ->
                                   (((p -> false) -> q) | ((p -> false) -> r)))
    Rule name [RIGHT_IMPLIES], conclusions [1], treating branch [1 of 1]
    Details: Eval(((p -> false) -> (q | r)),premise)= F
    Generated node: (1)
    | ((p -> false) -> (q | r))[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))
[2] ------------------------------------ [CLASH_DETECTION_RULE_APPLICATION]
    Stack size [0]
    Rule name: CLASH_DETECTION
    Clash status: FAILURE
[3] ------------------------------------ [META_RULE_APPLICATION]
    Stack size: [1], BACKTRACK POINT added
    Rule name [G3ibu Meta Backtrack rule], rules to try [2]
    Rule [1 of 2] selected, [LEFT_IMPLIES] on [->-formula]: ((p -> false) -> (q | r))
    Added [on rule resumed] listener for [G3ibu Meta Backtrack rule]
[4] ------------------------------------ [REGULAR_RULE_APPLICATION]
    Stack size: [2], AND-BRANCH POINT added
    Selected formula [->-formula]: ((p -> false) -> (q | r))
    Rule name [LEFT_IMPLIES], conclusions [2], treating branch [1 of 2]
    Generated node: (2)
    | (q | r)[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))
[5] ------------------------------------ [REGULAR_RULE_APPLICATION]
    Stack size: [3], AND-BRANCH POINT added
    Selected formula [|-formula]: (q | r)
    Rule name [LEFT_OR], conclusions [2], treating branch [1 of 2]
    Generated node: (3)
    | q[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))
[6] ------------------------------------ [CLASH_DETECTION_RULE_APPLICATION]
    Stack size [3]
    Rule name: CLASH_DETECTION
    Clash status: FAILURE
....

The output describes the iterations performed by the engine. Every iteration starts with a line of the form:

[N] ------------------------------------ [ENGINE_MOVE]

specifying that at iteration N the prover has performed the specified move. The possible moves are:

• INITIAL_STATE
• REGULAR_RULE_APPLICATION:
• CLASH_DETECTION_RULE_APPLICATION
• BRANCH_EXISTS_RULE_APPLICATION
• META_RULE_APPLICATION
• AND_BRANCH_POINT_SEARCH
• BACKTRACK_POINT_SEARCH

According with the move performed by the prover displays different data.

INITIAL_STATE

[0] ------------------------------------ [INITIAL_STATE]
    Stack size [0]
    Initial goal: (0)
    | [U]==>
    | (((p -> false) -> (q | r)) -> (((p -> false) -> q) | ((p -> false) -> r)))

The engine displays the initial stack size and the goal of the proof-search (having index 0). Node-sets are indexed by a counter displayed between (...) for future references.

REGULAR_RULE_APPLICATION

[4] ------------------------------------ [REGULAR_RULE_APPLICATION]
    Stack size: [2], AND-BRANCH POINT added
    Selected formula [->-formula]: ((p -> false) -> (q | r))
    Rule name [LEFT_IMPLIES], conclusions [2], treating branch [1 of 2]
    Generated node: (2)
    | (q | r)[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))

The engine displays the following data:

• The depth of the stack and a massage describing whether the performed rule application modified the stack.
• The treated formula (selected formula) that is the main formula of the rule application. For the formula are displayed both the short name that the formula description obtained by invoking the methods shortName() and format() of _AbstractFormula respectively.
• The applied rule, the number of conclusions generated by the rule application (conclusions [N]) and the conclusion treated by this rule application.
• The node-set generated by the rule application and selected as next goal.

CLASH_DETECTION_RULE_APPLICATION

[2] ------------------------------------ [CLASH_DETECTION_RULE_APPLICATION]
    Stack size [0]
    Rule name: CLASH_DETECTION
    Clash status: FAILURE

The engine displays the stack size, the rule name and the status of its application (FAILURE'' or ``SUCCESS).

BRANCH_EXISTS_RULE_APPLICATION

[8] ------------------------------------ [BRANCH_EXISTS_RULE_APPLICATION]
    Stack size: [4], BACKTRACK POINT added
    Selected formula [|-formula]: (((p -> false) -> q) | ((p -> false) -> r))
    Rule name [RIGHT_OR], conclusions [2], treating conclusion [1 of 2]
    Generated node: (4)
    | q[B]==>
    | ((p -> false) -> q)

The engine displays the following data:

• The depth of the stack and a massage describing whether the performed rule application modified the stack.
• The treated formula (selected formula) that is the main formula of the rule application.
• The applied rule, the number of conclusions generated by the rule application (conclusions [N]) and the conclusion treated by this rule application.
• The node-set generated by the rule application and selected as next goal.

META_RULE_APPLICATION

[36] ------------------------------------ [META_RULE_APPLICATION]
    Stack size: [2], BACKTRACK POINT added
    Rule name [G3ibu Meta Backtrack rule], rules to try [2]
    Rule [1 of 2] selected, [LEFT_IMPLIES] on [->-formula]: (p -> false)
    Added [on rule resumed] listener for [G3ibu Meta Backtrack rule]

The engine displays the following data:

• The depth of the stack and a massage describing whether the performed rule application modified the stack.
• The applied meta-backtrack rule with the number of rule applications generated by its application (rules to try [N]).
• The number of the rule selected for application, its name and its main formula.
• In the examples is also reported that applying the rule the engine registered an on rule resumed (this means that the applied meta-backtrack rule implements the engine._OnRuleResumedListener interface).

AND_BRANCH_POINT_SEARCH

[11] ------------------------------------ [AND_BRANCH_POINT_SEARCH]
    Stack size [2]
    Resumed AND-BRANCH point generated at iteration [5]
    Node set (2) generated at step [4]
    | (q | r)[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))
    Selected formula [|-formula]: (q | r)
    Rule name [LEFT_OR], conclusions [2], treating branch [2 of 2]
    Generated node: (6)
    | r[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))

If the stack does not contain any branch point, the proof-search successfully terminates. Otherwise, the prover displays the following data:

• The depth of the stack.
• The iteration that generated the resumed AND-branch point.
• The goal of the rule that generated the branch point (with details about its index and the iteration it was generated).
• The selected main formula.
• The applied rule and the conclusion treated by this rule application.
• The generate subgoal.

E.g., in the example, the rule that generated the AND-branch point was a LEFT_OR application treated at iteration 5 (where the first conclusion was generated). Now, the rule is resumed and its second (and last) conclusion is generated.

BACKTRACK_POINT_SEARCH

If the stack does not contain any backtrack point (OR-branch point), the proof-search unsuccessfully terminates. Otherwise, the prover displays some information about the restored branch-point. In this case the information provided depends on the type of the rule which added the backtrack-point.

In the backtrack-point was added by a branch-exists rule application, the prover displays:

[22] ------------------------------------ [BACKTRACK_POINT_SEARCH]
    Stack size [2]
    Resumed BACKTRACK point. Node set (6) generated at step [11]
    | r[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))
    Backtrack rule type [BRANCH_EXISTS]
    Selected formula [|-formula]: (((p -> false) -> q) | ((p -> false) -> r))
    Rule name [RIGHT_OR], conclusions [2], treating conclusion [2 of 2]
    Generated node: (11)
    | r[B]==>
    | ((p -> false) -> r)

• The depth of the stack.
• The goal of the rule that generated the branch point (with details about its index and the iteration it was generated).
• The selected main formula.
• The applied rule and the conclusion treated by this rule application.
• The generate subgoal.

If the backtrack-point was added by a meta-backtrack rule application, the prover displays:

[32] ------------------------------------ [BACKTRACK_POINT_SEARCH]
    Stack size [0]
    Resumed BACKTRACK point. Node set (1) generated at step [1]
    | ((p -> false) -> (q | r))[U]==>
    | (((p -> false) -> q) | ((p -> false) -> r))
    Backtrack rule type [META_BACKTRACK_RULE]
    Rule name [G3ibu Meta Backtrack rule], rules to try [2]
    Rule [2 of 2] selected, [RIGHT_OR] on [|-formula]: (((p -> false) -> q) | ((p -> false) -> r))

• The depth of the stack.
• The goal of the rule that generated the branch point (with details about its index and the iteration it was generated).
• The selected main formula.
• The applied metabacktrack rule, with the total number of rules.
• The rule selected for application with its name and main formula.