Launcher output explanation

The structure of the output of provers executed using the jtabwbx.lancher framework is independent of the specific prover. We describe such a structure using examples generated with the g3ibu prover. As input problem we use the Scott principle in the JTabWb format (see input specification).

Proof-search summary

Running the prover in non-verbose mode, we get a summary describing the essential facts about the performed proof-search. For example, running the prover X on the Scott principle, we get:

$ java -jar g3ibu-1.0.jar wffs/pitp_pitp_examples/scott 
> Parsing problem... time (ms) [120]
** Problem [Scott], status [UNPROVABLE]
> Building initial node set... time (ms) [3]
** Prover [gbu 1.0 (seq=bsf, eval=min)]
** Reader [pitpplain]
> Proving...
****************************************************************
** Prover [gbu 1.0 (seq=bsf, eval=min)]
** Problem [Scott], status [UNPROVABLE], proof-search [FAILURE], test [PASSED]
** Generated nodes [66], restored backtrack-points [8], restored branch-points [19]
** Timings (ms): PS (proof-search) [19], NSC (initial node set) [3], PP (problem parsing) [120]
** Proof time (PS + NSC + PP): (ms) [142]
****************************************************************

The output provides the following data:

• formula status is the status of the input formula (PROVABLE, UNPROVABLE or UNKNOWN).
• proof-search is the status of the proof-search (SUCCESS or FAILURE).
• test is the result of the test checking if the status of the formula and the result of the proof-search match. E.g., since g3ibu is a calculus for Intuitionistic provability the proof-search must fail for an unprovable formula and must succeed for a provable problem.
• The last two lines provide details on the prover execution.

Verbose mode output explanation

Running prover X in verbose mode (-va option) we get a detailed description of the performed proof-search. E.g., these are the first lines of the output of such an execution.

System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 48)

Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-1.txt’ not found or reading it failed

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
• BRANCH_POINT_SEARCH
• BACKTRACK_POINT_SEARCH

According to the move, the following data are displayed (the examples refer to the above execution):

• INITIAL_STATE The engine displays the initial node-set, that is the goal of the proof-search.

• REGULAR_RULE_APPLICATION The engine displays the following information:

  • The depth of the stack and if the stack has been modified by the rule application.
  • The main formula of the rule application (selected formula).
  • The short name of the formula, the name of the applied rule and the number of branches generated by the rule application (branches [N]). This coincides with the the number of conclusions of the regular-rule.
  • If specified, the details of the rule application (these details are provided by the user and specified in the implementation of the rule).
  • The branch treated by the rule, that is the index of the conclusion of the rule considered as next goal of the engine.
  • The node-set generated by the rule application and selected as next goal. Node-sets are referenced by a counter displayed between (...) for future references.

  E.g., this is an application of a regular rule with two conclusions.

  System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 95)

  Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-2.txt’ not found or reading it failed

• CLASH_DETECTION_RULE_APPLICATION The engine displays the stack size and the status of the clash-detection rule application (FAILURE'' or ``SUCCESS).

  System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 101)

  Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-3.txt’ not found or reading it failed

• BRANCH_EXISTS_RULE_APPLICATION

  • The depth of the stack and if the stack has been modified by the rule application.
  • The main formula of the rule application (selected formula).
  • The short name of the formula, the name of the applied rule and the number of backtrack branches generated by the rule application (branches [N]). This coincides with number of conclusions of the branch-exists rule.
  • If specified, the details of the rule application (these details are provided by the user and specified in the implementation of the rule).
  • The branch treated by the rule, that is the index of the conclusion of the rule considered as next goal of the engine.
  • The node-set generated by the rule application and selected as next goal.

  System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 122)

  Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-4.txt’ not found or reading it failed

• META_RULE_APPLICATION

  • The depth of the stack and if the stack has been modified by the rule application.
  • The name and the number of backtrack rules returned by the rule application (rules to try [N]).
  • The backtrack-rule treated by the rule and the details about the rule selected for application.

  System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 136)

  Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-5.txt’ not found or reading it failed

• BRANCH_POINT_SEARCH If the stack does not contain any branch point, the proof-search successfully terminates. Otherwise, the prover displays some information about the restored branch-point:

  • The depth of the stack.
  • Some information on the rule which pushed this branch-point on the stack: the premise of the rule, the main formula of the rule, the name of the rule and the number of conclusions of the rule.
  • The index of the treated branch.
  • The conclusion selected as new subgoal.

  System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 154)

  Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-6.txt’ not found or reading it failed

• BACKTRACK_POINT_SEARCH If the stack does not contain any 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 the following information:

  • The depth of the stack.
  • Some information on the branch-exists rule which pushed this backtrack-point on the stack: the premise of the rule, the main formula of the rule, the name of the rule and the number of conclusions of the rule.
  • The index of the treated branch.
  • The conclusion selected as new subgoal.

  System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 176)

  Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-7.txt’ not found or reading it failed

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

  • The depth of the stack.
  • The following information on the meta-backtrack rule which pushed the backtrack-point on the stack: the premise of the rule, the backtrack-rules to try.
  • The rule selected for application (name and main formula).

  System Message: WARNING/2 (/Users/ferram/git/_arc/fmsite/source/sw/output/output.rst, line 190)

  Include file u’/Users/ferram/git/_arc/fmsite/source/sw/output/g3ibu-va-ex-8.txt’ not found or reading it failed