Abstract of FKI-180-93

Document-Name:  FKI-180-93 (not available via ftp)
Title:	        Dependent-Deletion: A Refinement of Backward-Subsumption
Authors:	Christian B. Suttner, M. Lehmann 
                
Revision-Date:	1993/08/25 
Category:	Technical Report (Forschungsberichte Künstliche Intelligenz)
Abstract:	We present a refinement for backward-subsumption, which is
                an important technique to control the exponential search space 
		in theorem proving. The refinement basically prevents the
		generation of consequences which are known to be superflous,
		and thereby not only reduces the search space but also 
		reduces the amount of work required for removing such 
		consequences later (when their redundancy is detected).
Keywords:	automated theorem proving, resolution, backward-subsumption,
                redundancy control
Size:		6 pages
Language:	English
ISSN:		0941-6358
Copyright:	The ``Forschungsberichte Künstliche Intelligenz''
		series includes primarily preliminary publications,
		specialized partial results, and supplementary
		material. In the interest of a subsequent final
		publication these reports should not be copied. All
		rights and the responsability for the contents of the
		report are with the authors, which would appreciate
		critical comments.




Gerhard Weiss