Publications: Report

Technical, Research Report
@TechReport
Technischer-, Forschungsbericht

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

Options:

Goto entry point

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

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

Attachment Section