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.

• Type: Conference
• Year: 1990
• Where: CTRS
• Authors: Nachum Dershowitz
• Keywords: CTRS 1990, CTRS 1992, Equational Horn Clauses, Positive-unit Theorem-proving Procedure, Potentiallymaximal Sides