MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Jacobs, Swen
Waldmann, Uwe		dblp
dblp
Editor(s):
Beckert, Bernharddblp
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
Conference URL::
http://tableaux2005.uni-koblenz.de/
Downloading URL:
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
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


File Attachment Icon
InstGen-final.pdf