This class allows you to parse first order logic formulas. These formulas can be written in any syntax that you define.
You can apply basic logic operations (and, or, not, implies, etc...).
You can transform proposition (cleaning, developing, disjunctive form, conjunctive form).
You can even make demonstrations of your proposition, by looking up the values table or simply by demonstrating it (simple analysis of the disjunctive form: not too greedy).
The FOLP Checker allows you to prove that a proposition is a theorem, and if it is not, you will be presented a counterexample.
Karnaugh's table and other nice features will be soon added.
| Ratings | Utility |
Consistency |
Documentation |
Examples |
Tests |
Videos |
Overall |
Rank |
| All time: |
Good (83.3%) |
Sufficient (66.7%) |
- |
Sufficient (66.7%) |
- |
- |
Not sure (55.0%) |
1028 |
| Month: |
Not yet rated by the users |
| Link |
Description |
| online demo |
shows the test script in action |

If you know an application of this package, send a message to the
author to add a link here.
| File |
Role |
Description |
demo |
index.php |
Example |
The basic demo: showing the values table, normal forms, and can prove the given formula |
syntax.litteral |
Data |
Defines litteral syntax for the demo file (it then accepts two syntax, for example "a & b" is the same than "a AND b"). This is an example on how you can add your own supported syntax |
examples |
example1.php |
Example |
basic operations on propositions |
example2.php |
Example |
testing EQUALITY (and not equivalence) of formulas |
example3.php |
Example |
testing if propositions are in disjunctive/conjunctive forms |
example4.php |
Example |
Show cloning feature, and how to set values to variables in a proposition |
example5.php |
Example |
Shows how you can extend the base class to have nice HTML output of the values table |
example6.php |
Example |
Shows conjunctive/disjunctive forms of a proposition. You can see here that the computation time is a bit long :( |
FirstOrderLogicProp.inc.php |
Class |
The file containing base class and the checker class |