Gamma Exestentail Graph Therom Prover
Interactive theorem provers offer users a means of formalizing and proving logical and mathematical statements. Traditional interactive theorem provers, such as Hyperslate, Lazyslate, Athena, Lean, and others offer users the ability to prove theorems in a proof system called natural deduction which models how humans reason about finding proofs in natural language. Other proof systems such as axiom based Hilbert systems are smaller with a tradeoff that proofs are harder to find. One interesting proof system is Charles Sanders Peirce’s Existential Graph visual proof system, in which formulae are represented as 2d drawings, inference rules are transformations of these drawings, and proofs are linear (non-branching) sequences of transformations.
We are creating a gamma exestential graph therom prover because one does not currently exist. Gamma does not add very much additional complexity over alpaha exestential graphs while providing significant advantagages. Allowing the use of modal logic allows for a wider variety of applications for use of the application.