GraphProver is a theorem prover for Propositional Minimal Logic. In current development it implements only the implication connective.
GraphProver depends on the following libraries (listed with the versions I'm using):
- love (0.10.11)
- lpeg (1.0.0-1)
- lualogging (1.3.0-1)
Löve is a canvas for Lua game development that we use to build the prover user interface. It can be downloaded from the project website.
Lpeg is a pattern-matching library for Lua. We use lpeg to parse input formulae in our prover. It can be installed using luarocks.
lualogging is used to register log messages. It also can be installed using luarocks.
Inside SequentProver directory:
- Run the prover graphical interface
love .
- Follow commands in the graphical interface
Parentheses are required to the right side of every subformula.
The formula A → (B → A) has to be entered as:
A imp (B imp (A))