You are looking at historical revision 6720 of this page. It may differ significantly from its current revision.
This egg is for doing predicate calculus, to see whether a statement in predicate calculus is logically valid or not. The algorithm is guaranteed to terminate if the statement can be proven. The algorithm is resolution based.
Supported Quantifiers and Logical Connectives
"exist" means "there exists" "all" means "for all"
xor and or not => <=>