Sciweavers

RTA
1993
Springer

Redundancy Criteria for Constrained Completion

14 years 4 months ago
Redundancy Criteria for Constrained Completion
This paper studies completion in the case of equations with constraints consisting of rstorder formulae over equations, disequations, and an irreducibility predicate. We present several inference systems which show in a very precise way how to take advantage of redundancy notions in this framework. A notable feature of these systems is the variety of tradeo s they present for removing redundant instances of the equations involved in an inference. The irreducibility predicates simulate redundancy criteria based on reducibility such as prime superposition and Blocking in Basic Completion and the disequality predicates simulate the notion of subsumed critical pairs; in addition, since constraints are passed along with equations, we can perform hereditary versions of all these redundancy checks. This combines in one consistent framework stronger versions of all practical critical pair criteria. We also provide a rigorous analysis of the problem with completing sets of equations with ini...
Christopher Lynch, Wayne Snyder
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1993
Where RTA
Authors Christopher Lynch, Wayne Snyder
Comments (0)