system-L

Descripton

It's a formal logic deduction based on system-L

The three basic axioms:

{p,p->q} |- q

Read this book or click here to see more details.

To prove one proposition:

Firstly, Use deduction theorem to de-level the formula and get a proposition variable or a proposition in form of ~(...). Let's denote it as p or ~p.
Next, Create a set called garma and fill it with some generated formulas which is deduced from the above axioms, some theorems and conclusions.
Then, Search p or ~p in garma, or further, using modus ponent(MP) to deduce p or ~p.
Finally, if MP can't prove it, use Proof by contradiction instead.

python modules