Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

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

Action:

login to update

Options:








Author, Editor

Author(s):

Jacobs, Swen
Waldmann, Uwe

dblp
dblp



Editor(s):

Beckert, Bernhard

dblp

Not MPII Editor(s):

Beckert, Bernhard

BibTeX cite key*:

JacobsWaldmann2005

Title, Booktitle

Title*:

Comparing Instance Generation Methods for Automated Reasoning


InstGen-final.pdf (427.84 KB)

Booktitle*:

Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX 2005

Event, URLs

URL of the conference:

http://tableaux2005.uni-koblenz.de/

URL for downloading the paper:


Event Address*:

Koblenz, Germany

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

14 September 2005

Event End Date:

17 September 2005

Publisher

Name*:

Springer

URL:

http://www.springer.de

Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

3702

Number:


Month:


Pages:

153-168

Year*:

2005

VG Wort Pages:

29

ISBN/ISSN:

3-540-28931-3

Sequence Number:


DOI:




Note, Abstract, ©


(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.

HyperLinks / References / URLs:

http://www.springer.de/comp/lncs/index.html

Copyright Message:

Copyright 2005 Springer-Verlag


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Appearance:

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



BibTeX Entry:

@INPROCEEDINGS{JacobsWaldmann2005,
AUTHOR = {Jacobs, Swen and Waldmann, Uwe},
EDITOR = {Beckert, Bernhard},
TITLE = {Comparing Instance Generation Methods for Automated Reasoning},
BOOKTITLE = {Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX 2005},
PUBLISHER = {Springer},
YEAR = {2005},
VOLUME = {3702},
PAGES = {153--168},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Koblenz, Germany},
ISBN = {3-540-28931-3},
}


Entry last modified by Christine Kiesel, 12/21/2005
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
09/23/2005 11:19:23 AM
Revision
1.
0.


Editor
Christine Kiesel
Swen Jacobs


Edit Date
21.12.2005 10:46:41
23.09.2005 11:19:23


Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
InstGen-final.pdf