search

samanthajlee2 / ExistentialGraphProofGenerator

Generates Existential Graph Proofs from set of premises to a goal.
0 stars 1 forks source link

Setup the necessary parts for the proof generation #3

Closed sihsob closed 7 years ago

sihsob commented 7 years ago

Before generating the proof, some setup on the existential graph tree is needed is needed.

  1. Insert in double cut next to the root node that isn't SA
  2. Insert the negation (a cut) of the goal (conclusion) into the first level of the double cut just inserted
  3. Insert the a cut of the premise and the negation of the goal into the second level of the double cut (basically recreate an existential graph version of a subproof)

Once this is setup and the inserted into the proof generation algorithm, the resulting graph should be a cut of the conclusion negated and a double cut. The double cut can be removed which makes another double that can be removed which is the conclusion.

Note: Make sure to add these setup steps into the steps for the final proof generated

sihsob commented 7 years ago

Potentially buggy, but the setup should be complete by #16