On the use of constraints in automated deduction
- 1 January 1995
- book chapter
- Published by Springer Nature
- p. 128-146
- https://doi.org/10.1007/3-540-59155-9_8
Abstract
No abstract availableKeywords
This publication has 24 references indexed in Scilit:
- Rewrite-based Equational Theorem Proving with Selection and SimplificationJournal of Logic and Computation, 1994
- Narrowing based procedures for equational disunificationApplicable Algebra in Engineering, Communication and Computing, 1992
- A technical note on AC-Unification. The number of minimal unifiers of the equation ?x1 + ? + ?xp ?AC ?y1 + ? + ?yqJournal of Automated Reasoning, 1992
- Completion of rewrite systems with membership constraintsPublished by Springer Nature ,1992
- Basic paramodulation and superpositionPublished by Springer Nature ,1992
- Rewrite SystemsPublished by Elsevier ,1990
- Completion for rewriting modulo a congruenceTheoretical Computer Science, 1989
- Complete sets of reductions modulo associativity, commutativity and identityPublished by Springer Nature ,1989
- Completion of a Set of Rules Modulo a Set of EquationsSIAM Journal on Computing, 1986
- Termination orderings for associative-commutative rewriting systemsJournal of Symbolic Computation, 1985