Paramodulation with non-monotonic orderings and simplification
From MaRDI portal
Publication:352977
DOI10.1007/S10817-011-9244-ZzbMATH Open1315.03017OpenAlexW2041375296MaRDI QIDQ352977FDOQ352977
Authors: Miquel Bofill, Albert Rubio 
Publication date: 5 July 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9244-z
Recommendations
Cites Work
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
- Termination of term rewriting using dependency pairs
- Proving termination with multiset orderings
- Orderings for term-rewriting systems
- Term Rewriting and All That
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Title not available (Why is that?)
- Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- Title not available (Why is that?)
- Paramodulation-based theorem proving
- Paramodulation with Well-founded Orderings
- Equational inference, canonical proofs, and proof orderings
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated Reasoning
- Termination tools in ordered completion
Cited In (8)
- Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
- Equational theorem proving modulo
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated Reasoning
- Paramodulation with Well-founded Orderings
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
- A Lambda-Free Higher-Order Recursive Path Order
Uses Software
This page was built for publication: Paramodulation with non-monotonic orderings and simplification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q352977)
