Generic reasoning: Theorem-proving strategies
A theorem-proving strategy is defined by an inference system
and a search plan.
Ordering-based inference systems,
that evolved from resolution and Knuth-Bendix completion,
feature (ordered) resolution,
(ordered) paramodulation/superposition,
simplification or term rewriting and subsumption.
Subgoal-reduction-based inference systems,
that evolved from natural deduction and analytic tableaux,
are based on
model elimination and clause normalform tableaux.
Instance-based inference systems,
that evolved from the methods of Gilmore and Davis-Putnam,
are based on clause linking to generate instances rather than consequences.
Inference systems are non-deterministic and a deterministic strategy
is defined by adding a search plan that decides which inference to apply next.
Search plans can be either sequential or parallel.
Selected topics in my work on theorem proving include,
in reverse chronological order:
Maria Paola Bonacina