First-order theorem proving with equality is undecidable, in general.
is semi-decidable in the sense that it is refutationally complete. The
basis for a
(semi)-decision procedure for first-order clauses with equality is a
of inference and reduction rules. The inference rules of the calculus
new clauses whereas the reduction rules delete clauses or transform them
ones. If, in particular, strong reduction rules are available,
certain subclasses of first-order logic can be shown. Hence,
are essential for progress in automated theorem proving. In this thesis we
consider the superposition calculus and in particular the sophisticated
rule Contextual Rewriting. However, it is in general undecidable whether
rewriting can be applied. Therefore, to make the rule applicable in
it has to be further refined. In this work we develop an instance of
rewriting which effectively performs contextual rewriting and we
in the theorem prover Spass.