Completion-based and resolution-based theorem proving

The problem of combining forward and backward reasoning, or reasoning from the assumptions and reasoning from the target theorem, has been a fundamental problem since the birth of automated theorem proving: In my own research, I studied lemmaizing and caching techniques as a way of combining forward and backward reasoning in semantic resolution and model elimination: I also attacked this problem in completion-based theorem proving, formulating a framework, based on well-founded proof orderings, where completion procedures are semidecision procedures for theorem proving. The resulting theorem-proving strategies are target-oriented and contraction-based. The notions of proof reduction, fairness, and redundancy become target-oriented. Contraction-based strategies have an inference system with contraction rules and an eager-contraction search plan. Contraction rules delete or replace redundant clauses, as in subsumption and simplification, while expansion rules, such as resolution and paramodulation/superposition, only generate clauses. Eager contraction keeps the database of clauses as small as possible, which is critical to prove theorems such as the "Dependency of the Fifth Axiom" in Lukasiewicz's many-valued logic: I also worked on rewrite programs interpreted by Linear Completion, showing that they are not equivalent to Prolog: Earlier versions of the work on completion appeared in my PhD and doctoral theses.


Maria Paola Bonacina