Sciweavers

138
Voted
CTRS
1990
15 years 11 months ago
A Simplifier for Untyped Lambda Expressions
Louis Galbiati, Carolyn L. Talcott
146
Voted
CTRS
1990
15 years 11 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
194
Voted
CTRS
1990
15 years 11 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
159
Voted
CTRS
1990
15 years 11 months ago
Extended Term Rewriting Systems
Jan Willem Klop, Roel C. de Vrijer