Technical, Research Report
@TechReport
Technischer-, Forschungsbericht


Show entries of:

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

Action:

login to update

Options:









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):





BibTeX Citekey*:

GeorgievaHustadtSchmidt02c

Language:

English

Title, Institution

Title*:

A New Clausal Class Decidable by Hyperresolution

Institution*:

University of Manchester

Publishers or Institutions Address*:

UK

Type:

Preprint Series

No, Year, pp.,

Number*:

CSPP-18

Pages*:

19

Month:

July

VG Wort
Pages*:

30

Year*:

2002

ISBN/ISSN:






DOI:




Note, Abstract, ©

Note:

Long version of~\cite{GeorgievaHustadtSchmidt02b}.

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

Categories / Keywords:

Theorem Proving

Copyright Message:


HyperLinks / References / URLs:

http://www.cs.man.ac.uk/~schmidt/publications/GeorgievaHustadtSchmidt02c.html

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:
@TECHREPORT{GeorgievaHustadtSchmidt02c,
AUTHOR = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
TITLE = {A New Clausal Class Decidable by Hyperresolution},
YEAR = {2002},
TYPE = {Preprint Series},
INSTITUTION = {University of Manchester},
NUMBER = {CSPP-18},
PAGES = {19},
ADDRESS = {UK},
MONTH = {July},
NOTE = {Long version of~\cite{GeorgievaHustadtSchmidt02b}.},
}


Entry last modified by Christine Kiesel, 03/12/2010
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)
Renate A. Schmidt
Created
02/03/2003 06:21:57 PM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Renate A. Schmidt
Renate A. Schmidt
Edit Dates
01.09.2003 17:24:07
01.09.2003 16:39:32
29.07.2003 14:33:43
05/07/2003 11:55:46 AM
05/07/2003 11:55:06 AM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section