Sciweavers

58
Voted
CTRS
1990
15 years 2 months ago
A Simplifier for Untyped Lambda Expressions
Louis Galbiati, Carolyn L. Talcott
CTRS
1990
15 years 2 months ago
A Maximal-Literal Unit Strategy for Horn Clauses
A new positive-unit theorem-proving procedure for equational Horn clauses is presented. It uses a term ordering to restrict paxamodulation to potentiallymaximal sides of equations...
Nachum Dershowitz
79
Voted
CTRS
1990
15 years 2 months ago
Completion Procedures as Semidecision Procedures
Completion procedures, originated from the seminal work of Knuth and Bendix, are wellknown as procedures for generating confluent rewrite systems, i.e. decision procedures for al ...
Maria Paola Bonacina, Jieh Hsiang
69
Voted
CTRS
1990
15 years 2 months ago
Extended Term Rewriting Systems
Jan Willem Klop, Roel C. de Vrijer
CTRS
1992
15 years 2 months ago
Path Orderings for Termination of Associative-Commutative Rewriting
We show that a simple, and easily implementable, restriction on the recursive path ordering, which we call the "binary path condition," sufficesfor establishing terminat...
Nachum Dershowitz, Subrata Mitra
CTRS
1992
15 years 2 months ago
Decidability of Regularity and Related Properties of Ground Normal Form Languages
ded abstract of this paper is published in the proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems, Pont- -Mousson, 1992 1
Gregory Kucherov, Mohamed Tajine