Improved Redundancy Criteria and their implementation
Hans de Nivelle
In this talk I give an overview of recent research into
redundancy criteria for clauses.
It is well-known that deletion of subsumed clauses improves the
behaviour of a resolution theorem prover dramatically.
A similar improvement is obtained by adding rewrite-simplification for
theorem proving with equality.
In this talk I explain how more general redundancy criteria can be obtained,
and how they can be implemented.
Christoph Benzmüller,
chris@ags.uni-sb.de
Last modified: Wed Sep 13 19:55:42 MEST 2000