Publications: Unpublished/Draft

Unpublished, Draft, To Appear
@UnPublished
Unveröffentlicht, Entwurf

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

Options:

Goto entry point

Author, Editor

Author(s):

Ohlbach, Hans Jürgen

dblp

BibTeX citekey*:

Ohlbach95a

Title, Booktitle

Title*:

Clause Killer Transformations

Vol, No, pp., Year

Month:		Year:	1995
Language:	English	Pages:

Abstract, Links, ©

Note:	Submitted to the Journal of Automated Reasoning
LaTeX Abstract:	It is shown how self resolving clauses like the transitivity clause or the condensed detachment clause can be deleted from the clause set by generating not all, but sufficiently many resolvents with the self resolving clause. Using this technique I found dramatic improvements of the performance of automated theorem provers on extremely hard problems. As by--products we get a method for encoding some axioms in Prolog which normally would generate loops, and we get a method for parallelizing some closure computation algorithms.
Categories / Keywords:
HyperLinks / References / URLs:
Personal Comments:
File Upload:

Download Access Level:	Public

Correlation

MPG Unit:	Max-Planck-Institut für Informatik

MPG Subunit:	Programming Logics Group
Audience:	Expert
Appearance:

BibTeX Entry:

@UNPUBLISHED{Ohlbach95a,
AUTHOR = {Ohlbach, Hans J{\"u}rgen},
TITLE = {Clause Killer Transformations},
YEAR = {1995},
NOTE = {Submitted to the Journal of Automated Reasoning},
}

Entry last modified by Christine Kiesel, 03/12/2010

Edit History (please click the blue arrow to see the details)

	Editor(s) Hans Jürgen Ohlbach	Created 02/06/1995 05:56:20 PM
Revisions 4. 3. 2. 1. 0.	Editor(s) Christine Kiesel Christine Kiesel Uwe Brahm/MPII/DE Christine Kiesel/AG2/MPII/DE Christine Kiesel/AG2/MPII/DE	Edit Dates 16.09.2003 15:26:03 27.03.2001 10:58:26 AM 10/02/95 17:20:10 09/02/95 10:27:05 31/01/95 15:47:27

Attachment Section