Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor(s)

Author(s):

Jacobs, Swen
Waldmann, Uwe

dblp
dblp



BibTeX cite key*:

JacobsWaldmann2007

Title

Title*:

Comparing Instance Generation Methods for Automated Reasoning

Journal

Journal Title*:

Journal of Automated Reasoning

Journal's URL:

http://www.springerlink.com/content/1573-0670/

Download URL
for the article:

http://dx.doi.org/10.1007/s10817-006-9046-x

Language:

English

Publisher

Publisher's
Name:

Springer

Publisher's URL:

http://www.springerlink.com/

Publisher's
Address:


ISSN:

0168-7433

Vol, No, pp, Date

Volume*:

38

Number:

1/3

Publishing Date:

April 2007

Pages*:

57-78

Number of
VG Pages:

44

Page Start:

57

Page End:

78

Sequence Number:


DOI:

10.1007/s10817-006-9046-x

Note, Abstract, ©

Note:


(LaTeX) Abstract:

The clause-linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the disconnection tableau calculus, and saturation-based methods, such as primal partial instantiation and resolution-based instance generation. We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one.

URL for the Abstract:

http://www.springerlink.com/content/c5380ju434580872/

Categories,
Keywords:

Theorem Proving, Disconnection Calculus, Resolution-based Instance Generation, Primal Partial Instantiation

HyperLinks / References / URLs:


Copyright Message:

Copyright 2007 Springer Netherlands

Personal Comments:


Download
Access Level:

Intranet

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:

@ARTICLE{JacobsWaldmann2007,
AUTHOR = {Jacobs, Swen and Waldmann, Uwe},
TITLE = {Comparing Instance Generation Methods for Automated Reasoning},
JOURNAL = {Journal of Automated Reasoning},
PUBLISHER = {Springer},
YEAR = {2007},
NUMBER = {1/3},
VOLUME = {38},
PAGES = {57--78},
MONTH = {April},
ISBN = {0168-7433},
DOI = {10.1007/s10817-006-9046-x},
}


Entry last modified by Uwe Brahm, 03/28/2008
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Swen Jacobs
Created
03/06/2007 12:38:49 PM
Revisions
4.
3.
2.
1.
0.
Editor(s)
Uwe Brahm
Anja Becker
Christine Kiesel
Swen Jacobs
Swen Jacobs
Edit Dates
03/28/2008 06:11:34 PM
13.02.2008 15:58:37
12.07.2007 10:32:58
13.04.2007 10:42:41
06.03.2007 12:38:49