Handbook of Automated Reasoning

Get full access to Handbook of Automated Reasoning and 60K+ other titles, with a free 10-day trial of O'Reilly.

There are also live events, courses curated by job role, and more.

5.3 Jouannaud and Kounalis approach [Jouannaud and Kounalis 1989]

We show here a slight extension of the Jouannaud and Kounalis and of Dershowitz [1989] approach. Now, we do not assume any set of free constructors nor any equality predicate. Instead, we assume that the axioms of the specifications are oriented into a finite (ground) convergent rewrite system $R_{0}$ Examples 3.1 and 2.7 are easy to complete in order to satisfy this condition.

$A$ contains all disequalities s ≠ t for terms s,t such that s t and s is not reducible. ...

Get Handbook of Automated Reasoning now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial

Don’t leave empty-handed

Get Mark Richards’s Software Architecture Patterns ebook to better understand how to design components—and how they should interact.

It’s yours, free.

Get it now

Check it out now on O’Reilly

Dive in for free with a 10-day trial of the O’Reilly learning platform—then explore all the other resources our members count on to build skills and solve problems every day.

Start your free trial Become a member now