Teaching Automated Theorem Proving by Example: PyRes 1.2
                     (system description)

                 Stephan Schulz and Adam Pease

PyRes is a complete theorem prover for classical first-order
logic. It is not designed for high performance, but to clearly
demonstrate the core concepts of a saturating theorem prover. The
system is written in extensively commented Python, explaining data
structures, algorithms, and many of the underlying theoretical
concepts. The prover implements binary resolution with factoring and
optional negative literal selection. Equality is handled by adding
the basic axioms of equality. PyRes uses the given-clause algorithm,
optionally controlled by weight- and age evaluations for clause
selection. The prover can read TPTP CNF/FOF input files and produces
TPTP/TSTP proof objects.

Evaluation shows, as expected, mediocre performance compared to
modern high-performance systems, with relatively better performance
for problems without equality. However, the implementation seems to
be sound and complete.