TL;DR
This paper investigates how various proof orderings influence the concept of saturation in automated reasoning, connecting different proof techniques and reduction methods to these orderings.
Contribution
It provides a formal analysis linking proof orderings with saturation, completion, paramodulation, and rewrite system reduction, clarifying their interrelations.
Findings
Different proof orderings induce distinct saturation notions
Connections established between completion, paramodulation, and rewrite reduction
Framework for understanding proof transformations based on orderings
Abstract
We explore how different proof orderings induce different notions of saturation. We relate completion, paramodulation, saturation, redundancy elimination, and rewrite system reduction to proof orderings.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Distributed systems and fault tolerance