On using ground joinable equations in equational theorem proving
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 1552512 (Why is no real title available?)
- scientific article; zbMATH DE number 1392288 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Complete Sets of Reductions for Some Equational Theories
- Complete sets of reductions with constraints
- On ground-confluence of term rewriting systems
- Ordered rewriting and confluence
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- The CADE-16 ATP system competition
- The TPTP problem library. CNF release v1. 2. 1
- Theorem proving with ordering and equality constrained clauses
- Towards a foundation of completion procedures as semidecision procedures
Cited in
(11)- AC simplifications and closure redundancies in the superposition calculus
- Extending Maximal Completion (Invited Talk)
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Twee: an equational theorem prover
- Implementing Superposition in iProver (System Description)
- Automated Reasoning
- Ground joinability and connectedness in the superposition calculus
- scientific article; zbMATH DE number 1765706 (Why is no real title available?)
- Certified equational reasoning via ordered completion
- Computer Science Logic
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
This page was built for publication: On using ground joinable equations in equational theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1404987)
