You are looking at historical revision 6720 of this page. It may differ significantly from its current revision.

Introduction

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

Quantifiers:

"exist"  means "there exists"
"all"    means "for all"

Logical Connectives:

xor and or not => <=>