A new positive-unit theorem-proving procedure for equational Horn clauses is presented. It uses a term ordering to restrict paramodulation to potentially maximal sides of equations. Completeness is shown using proof orderings.
This research supported in part by the National Science Foundation under Grant CCR-9007195.