Teaching Automated Theorem Proving by Example: PyRes 1.2

DOI10.1007/978-3-030-51054-1_9OpenAlexW3038874144MaRDI QIDQ5048999

Stephan Schulz, Adam Pease

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_9

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

PyRes ⋮ Unnamed Item

Uses Software

• VAMPIRE
• SPASS
• Prover9
• Mace4
• StarExec
• iProver
• leanCoP
• ileanCoP
• E Theorem Prover

Cites Work

• Unnamed Item
• Faster, higher, stronger: E 2.3
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Teaching Automated Theorem Proving by Example: PyRes 1.2