MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Georgieva, Lilia
Hustadt, Ullrich
Schmidt, Renate A.		dblp
dblp
dblp
Not MPG Author(s):
Georgieva, Lilia
Hustadt, Ullrich
Schmidt, Renate A.
Editor(s):
Voronkov, Andreidblp
Not MPII Editor(s):
Voronkov, Andrei
BibTeX cite key*:
GeorgievaHustadtSchmidt02b
Title, Booktitle
Title*:
A New Clausal Class Decidable by Hyperresolution
Booktitle*:
Automated deduction, CADE-18 : 18th International Conference on Automated Deduction
Event, URLs
Conference URL::
http://www.uni-koblenz.de/~cade-18/
Downloading URL:
Event Address*:
Copenhagen, Denmark
Language:
English
Event Date*
(no longer used):
-- July,27-30, 2002
Organization:
Event Start Date:
27 July 2002
Event End Date:
30 July 2002
Publisher
Name*:
Springer
URL:
Address*:
Heidelberg, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Artificial Intelligence
Volume:
2392
Number:
Month:
Pages:
260-274
Year*:
2002
VG Wort Pages:
ISBN/ISSN:
3-540-43931-5
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
In this paper we define a new clausal class, called $\mathcal{BU}$, which
can be decided by hyperresolution with splitting.
We also consider the model generation problem for $\mathcal{BU}$ and
show that hyperresolution plus splitting can also be used as a Herbrand
model generation procedure for $\mathcal{BU}$ and, furthermore, that the addition
of a local minimality test allows us to generate only minimal Herbrand
models for clause sets in $\mathcal{BU}$.
In addition, we investigate the relationship of $\mathcal{BU}$ to other
solvable classes.
URL for the Abstract:
http://www.cs.man.ac.uk/~schmidt/publications/GeorgievaHustadtSchmidt02c.html
Keywords:
Theorem Proving, decidability, model computation
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
Expert
Appearance:



BibTeX Entry:
@INPROCEEDINGS{GeorgievaHustadtSchmidt02b,
AUTHOR = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 EDITOR = {Voronkov, Andrei},
 TITLE = {A New Clausal Class Decidable by Hyperresolution},
 BOOKTITLE = {Automated deduction, CADE-18 : 18th International Conference on Automated Deduction},
 PUBLISHER = {Springer},
 YEAR = {2002},
 VOLUME = {2392},
 PAGES = {260--274},
 SERIES = {Lecture Notes in Artificial Intelligence},
 ADDRESS = {Copenhagen, Denmark},
 ISBN = {3-540-43931-5},
}

Entry last modified by Christine Kiesel, 03/12/2010
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)
Renate A. Schmidt		Created
02/03/2003 06:16:34 PM
Revisions
11.
10.
9.
8.
7.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
01.09.2003 17:24:34
01.09.2003 16:40:12
01.09.2003 14:20:00
01.08.2003 15:48:32
29.07.2003 14:34:41