-
Notifications
You must be signed in to change notification settings - Fork 1
System PyRes
Stephan Schulz, Adam Pease
PyRes is a pedagogical theorem prover (or, more correctly, family of theorem provers) for first order predicate logic. There are three systems of increasing complexity: a minimal resolution-based prover for clause logic, a prover for clause logic with refined calculus, heuristics, and indexing, and finally the main prover, which adds a clausifier and support for full first order logic with equality. Equality is handled by automatically adding suitable axioms for the given signature.
The code is extensively documented in a literate programming style and has nearly full coverage by unit tests. The main prover can also produce TSTP-compliant proof objects.
- Proving
- Model finding
PyRes supports most of the CNF and FOF languages of TPTP-3, with the exception of strings as distinct objects.
PyRes follows the SZS reporting standard.
PyRes supports most of the CNF and FOF languages of TPTP-3. . //: # "Format-Out-TPTP"
[https://github.com/eprover/PyRes] (https://github.com/eprover/PyRes)
E is implemented in Python, and should run on most current Python-3 versions.
The prover is Free/Open Source software and is licensed under the GNU GPL 2.
Maintained
Stephan Schulz, Adam Pease: Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description), Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR'20). Volume 12167 of LNAI. Springer, 2020. https://doi.org/10.1007/978-3-030-51054-1_9