MathLogic

Parser & proof checker and transformer for Logical Calculus.

Usage:

java -jar MathLogic.jar --%option% input output
options:

• --compile
  Compiles input file (see Fromat section).
• --deduct
  Makes one step of deduction on an input. Prints result to output. If there are no assumptions left, the proof will be checked.
• --sqr
  Given that the input file contains a number a, prints proof for (a + 1) * (a + 1) = a * a + 2 * a + 1

Format:

A proof can include another proof:

#use localFilePath ; targetFormula ; (variable to expression;)* localFilePath is the path to proof you want to use to prove targetFormula. If there is some ambiguity, you can fix it by assigning expressions to variables of the proof (only if proof is really going to be set there).

Proof usage is defined in it's header.

There is one header you MUST write.
#match formula
This is the formula to which targetFormula is matched in #use.

To apply N deduction steps, write
#deduct N

You might not want to do a naive replacement of the line with proof, since resulting proof length will grow exponentially. If there is no Generaliation(Each) rule involved in your proof, you can specify that it should be generalzied and later used with axiom @phi->phi[x:=o]. To do so, place
#each in the header