Equation solving in conditional AC-theories | Zendy

Nachum Dershowitz | Zendy; Subrata Mitra | Zendy; G. Sivakumar | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Equation solving in conditional AC-theories

Author(s) -

Nachum Dershowitz,

Subrata Mitra,

G. Sivakumar

Publication year - 1990

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-53162-9

DOI - 10.1007/3-540-53162-9_46

Subject(s) - unification , computer science , commutative property , associative property , equation solving , transformation (genetics) , algebra over a field , extension (predicate logic) , equational logic , theoretical computer science , mathematics , algorithm , mathematical optimization , programming language , discrete mathematics , differential equation , pure mathematics , rewriting , mathematical analysis , biochemistry , chemistry , gene

Conditional Equational Programming is an elegant way to uniformly integrate important features of functional and logic programming. Efficient methods 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 ad- vantages of both basic narrowing and normal narrowing. Another new feature, introduced in this paper, is the extension of equation solving to theories with defined functions that are associative and commutative, without using the costly AC.unification operation. This method has been implemented within SUTRA, a theorem proving and equational program- ming environment based on rewrite techniques and completion.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research