Equation Solving in Conditional AC-Theories

Conditional Equational Programming is an elegant way to uniformly integrate important features of functional and logic programming. Efficientmethods for equation solving are thus of great importance. In this paper, we formulate, and prove sound and complete, an equation solving procedure based on transformation rules. This method achieves a top-down, goal-directed strategy based on decomposition and restructuring, while preserving the advantages of both basicnarrowing and normalnarrowing. Another new feature, introduced in this paper, is the extension of equation solving to theories with defined functions that are associativeand commutative, without using the costly AC.unification operation. This method has been implemented within SUTRA, a theorem proving and equational programming environment based on rewrite techniques and completion.

• Type: Conference
• Year: 1990
• Where: ALP
• Authors: Nachum Dershowitz, Subrata Mitra, G. Sivakumar
• Keywords: ALP 1990, Automated Reasoning, Conditional Equational Programming, Equation Solving, Equational Programming