This code implements simple, resolution-based theorem provers for first-order logic. It is released as free software under the GNU GPL version 2, and without any warranty. See the file COPYING for details and the individual source headers for copyright information. Installation: ============= Just clone the repository into a new directory, with e.g. git clone https://github.com/eprover/PyRes.git No futher installation should be necessary. If you are on a UNIX-like OS (including Linux or macOS/OS-X), and "python3" is not in your standard search path (or not Python 3), you may need to edit the #!-line at the beginning of the three main programs (see below), or in all modules if you want to run the unit tests. pyres-simple.py =============== This is the simplest example of a prover for the clausal fragment of first-order logic. It implements the basic given-clause loop with first-in-first-out clause selection and without any redundancy elimination. Suggested command line: ./pyres-simple.py EXAMPLES/PUZ002-1.p PUZ001-1.p is quite hard for pyres-simple! pyres-cnf.py =========== This version of the prover processes the same logic as pyres-simple.py, but adds some performance-enhancing features. This include better clause selection heuristics, subsumption, and negative literal selection. Suggested command line: ./pyres-cnf.py -tfb -HPickGiven5 -nsmallest EXAMPLES/PUZ001-1.p pyres-fof.py =========== This prover adds a simple clausifier, so it is able to process full first-order logic. It also will detect the use of equality, and add equality axioms. Otherwise, it is similar to pyres-cnf.py. Suggested command line: ./pyres-fof.py -tifbp -HPickGiven5 -nlargest EXAMPLES/PUZ001+1.p ======== Information for CASC ================= The system comes as a zip file in StarExec compatible format. It requires (any) Python3 as python3. The StarExec package can be regenerated by "make starexec". THIS WILL OVERWRITE $(HOME)/StarExec WITHOUT FURTHER WARNING. You can change the build path in the Makefile. The runscript is starexec_run_PyRes_default Problem is CNF and unsatisfiable: # SZS status Unsatisfiable Problem is CNF and satisfiable: # SZS status Satisfiable Problem is FOF and a theorem: # SZS status Theorem Problem is FOF and not a theorem: # SZS status CounterSatisfiable The start of solution output for proofs: # SZS output start CNFRefutation. The end of solution output for proofs: # SZS output end CNFRefutation. The start of solution output for models/saturations: # SZS output start Saturation. The end of solution output for models/saturations: # SZS output end Saturation.