Adam Holsinger
5/3/2021
The argument prover accepts files in the .bram format. Within a proof block, it will read in all assumptions and goals and prove whether the argument holds for each goal. Included is a helpful utility to generate arguments; argument_generator.py will walk a user through all the steps needed to generate an argument that can be read by the proof generator.
After the argument file is generated, running main.py will start the main algorithm. After being told where to find the argument file, it will generate a file called <argument_name>_proof.bram (if there were multiple goals, it will generate multiple files with different numbers attached).
The first proof block (id="0") will contain all the assumptions and negated goal, as well as the final result of whether the whole tree was closed or open. If the tree was closed, the argument holds, if it was open, the argument does not hold. Each additional proof block corresponds to a branch from the original block, and that branch is indicated with a step labeled with the rule "BRANCH". Here is the meaning of the steps with a given rule:
Breakdown <Something> - A logical statement broken down into its component parts based on truth tree rules. The premise tag points to the step/assumption that was broken down to form this step.
BRANCH - A branch action was performed. Each premise tag points to the id of the proof blocks corresponding to this set of branches.
CLOSED-END - The branch was closed because a contradiction was found. The two contradicting steps are pointed to in the premise tags.
CLOSED - All branches generated by this branch were closed, so the closed branch propagates upwards. The premise tags point to the ids of the two closed proof branches.
OPEN-END - All statements were fully broken down and no contradictions were found, so the branch is open.
OPEN - A child branch was found to be open, so this branch is also open. Its premise tag points to the open child branch.