## Target-oriented completion-based theorem proving

A fundamental problem in the design of theorem-proving strategies is how to
combine *forward reasoning* (reasoning from the axioms) and
*backward reasoning* (reasoning from the goal).
This problem is especially challenging in *equational reasoning*:
when reasoning with equations, it is not sufficient to
reason from the goal; one needs to generate equations from equations
by paramodulation/superposition and inter-reduce them by rewriting.
Intuitively, this is because one needs to keep into account the
properties of equality.

I formulated a framework, based on well-founded proof orderings, for
*target-oriented strategies*,
interpreting *completion procedures*
(e.g., in the sense of *Knuth-Bendix*) as *semidecision procedures*.
It provides definitions that are target-oriented (i.e., relative to the
target theorem) for all fundamental notions in this sort of theorem proving,
such as *proof reduction*, *fairness* and *redundancy*:
- Maria Paola Bonacina and Jieh Hsiang.
Towards
a foundation of completion procedures as semidecision procedures.
Theoretical
Computer Science, 146:199-242, July 1995;
DOI: 10.1016/0304-3975(94)00187-N.

- Maria Paola Bonacina and Jieh Hsiang.
On fairness of
completion-based theorem proving strategies.
*Proceedings of the Fourth Conference on Rewriting Techniques and Applications (RTA)*,
Springer,
Lecture Notes in Computer Science 488, 348-360, 1991;
DOI: 10.1007/3-540-53904-2_109.

- Maria Paola Bonacina and Jieh Hsiang.
Completion
procedures as semidecision procedures.
*Proceedings of the Workshop on Conditional and Typed Rewriting Systems (CTRS) 1990*,
Springer,
Lecture Notes in Computer Science 516, 206-232, 1991;
DOI: 10.1007/3-540-54317-1_92.

Earlier versions of part of this work appeared in my PhD and doctoral theses.

*Maria Paola Bonacina*