On restrictions of ordered paramodulation with simplification
From MaRDI portal
Recommendations
Cites work
- Completion of first-order clauses with equality by strict superposition
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 4053061 (Why is no real title available?)
- scientific article; zbMATH DE number 4064978 (Why is no real title available?)
- scientific article; zbMATH DE number 4090851 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- Proving refutational completeness of theorem-proving strategies
- The Concept of Demodulation in Theorem Proving
Cited in
(33)- Order-sorted completion: The many-sorted way
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Basic paramodulation
- A complete and terminating approach to linear integer solving
- Extensional higher-order paramodulation in Leo-III
- Paramodulation with non-monotonic orderings and simplification
- I-terms in ordered resolution and superposition calculi: retrieving lost completeness
- scientific article; zbMATH DE number 176740 (Why is no real title available?)
- scientific article; zbMATH DE number 1303343 (Why is no real title available?)
- scientific article; zbMATH DE number 1324442 (Why is no real title available?)
- scientific article; zbMATH DE number 1348470 (Why is no real title available?)
- scientific article; zbMATH DE number 1754647 (Why is no real title available?)
- scientific article; zbMATH DE number 2090319 (Why is no real title available?)
- From search to computation: redundancy criteria and simplification at work
- Goal directed strategies for paramodulation
- Regular substitution sets: A means of controlling E-unification
- The search efficiency of theorem proving strategies
- Ordered chaining for total orderings
- Associative-commutative deduction with constraints
- Automated Reasoning
- Inductive theorem proving by consistency for first-order clauses
- Conditional term rewriting and first-order theorem proving
- Completion of first-order clauses with equality by strict superposition
- Clausal rewriting
- A comprehensive framework for saturation theorem proving
- A comprehensive framework for saturation theorem proving
- Superposition with Delayed Unification
- Positive deduction modulo regular theories
- Towards a foundation of completion procedures as semidecision procedures
- A modular formalization of superposition in Isabelle/HOL
- Exploiting instantiations from paramodulation proofs in Isabelle/HOL
- Partial redundancy in saturation
- A completion procedure for conditional equations
This page was built for publication: On restrictions of ordered paramodulation with simplification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6488549)
