Sciweavers

CTRS
1990

A Maximal-Literal Unit Strategy for Horn Clauses

14 years 3 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. Completeness is shown using proof orderings.
Nachum Dershowitz
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1990
Where CTRS
Authors Nachum Dershowitz
Comments (0)