Affiliations: Department of Mathematics and Computer Science, Clarkson University, Box 5815, Potsdam, NY 13699-5815, USA. [email protected] | LORIA, BP 239, 54506 Vandoeuvre-les-Nancy Cedex, France. [email protected]
Note: [] Address for correspondence: Department of Mathematics and Computer Science, Clarkson University, Box 5815, Potsdam, NY 13699-5815, USA
Note: [] Address for correspondence: LORIA, BP 239, 54506 Vandoeuvre-les-Nancy Cedex, France
Abstract: We give a new simplification method, called E-cycle Simplification, for Basic Completion inference systems. We prove the completeness of Basic Completion with E-cycle Simplification. We prove that E-cycle Simplification is strictly stronger than the only previously known complete simplification method for Basic Completion, Basic Simplification, in the sense that every derivation involving Basic Simplification is a derivation involving E-cycle Simplification, but not vice versa. E-cycle Simplification is simple to perform, and does not use the reducibility-relative-to condition. ECC implements our method.
