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: Earlier versions of part of this work appeared in my PhD and doctoral theses.



Maria Paola Bonacina