PyLogic

PyLogic is a tool for theorem proving implemented in Python 3.

Dependences

• Python 3
• pip
• PyQt4
• ply (automatically installed with pip)

Quickstart

Ensure that dependences are installed before.

git clone [email protected]:b3aver/PyLogic.git
cd PyLogic
make

Propositional Formulas

The grammar for specify a propositional formula is

formula : LETTER
        | NOT formula
        | ( formula CONNECTIVE formula )

where LETTER is an uppercase letter of the English alphabet, NOT is the minus sign -, and CONNECTIVE is one of the following symbols

• | or
• & and
• -> implication
• <- converse implication
• <-> biconditional

Testing

The package includes several tests written with unittest. These tests can be executed with make test also if Travis says that the current state is

References

• Melvin Fitting. First-Order Logic and Automated Theorem Proving.