A New Clausal Class Decidable by Hyperresolution

L. Georgieva; Ullrich Hustadt; R.A. Schmidt

A New Clausal Class Decidable by Hyperresolution

L. Georgieva, Ullrich Hustadt, R.A. Schmidt

University of Liverpool

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

Abstract

In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.

Original language	English
Title of host publication	Automated Deduction - CADE-18
Subtitle of host publication	18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings
Editors	Andrei Voronkov
Place of Publication	Heidelberg
Publisher	Springer Berlin
Pages	260-274
Number of pages	15
ISBN (Electronic)	9783540456209
ISBN (Print)	9783540439318
Publication status	Published - 17 Jul 2002

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2392

Keywords

Modal Logic
Description Logic
Predicate Symbol
Direct Successor
Unit Clause

Cite this

@inbook{b37f1fdaa51446d0a656653d8a1b794b,

title = "A New Clausal Class Decidable by Hyperresolution",

abstract = "In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.",

keywords = "Modal Logic, Description Logic, Predicate Symbol, Direct Successor, Unit Clause",

author = "L. Georgieva and Ullrich Hustadt and R.A. Schmidt",

year = "2002",

month = jul,

day = "17",

language = "English",

isbn = "9783540439318",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin",

pages = "260--274",

editor = "Voronkov, {Andrei }",

booktitle = "Automated Deduction - CADE-18",

address = "Germany",

}

A New Clausal Class Decidable by Hyperresolution. / Georgieva, L.; Hustadt, Ullrich; Schmidt, R.A.
Automated Deduction - CADE-18: 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings. ed. / Andrei Voronkov. Heidelberg: Springer Berlin, 2002. p. 260-274 (Lecture Notes in Computer Science; Vol. 2392).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - A New Clausal Class Decidable by Hyperresolution

AU - Georgieva, L.

AU - Hustadt, Ullrich

AU - Schmidt, R.A.

PY - 2002/7/17

Y1 - 2002/7/17

N2 - In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.

AB - In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.

KW - Modal Logic

KW - Description Logic

KW - Predicate Symbol

KW - Direct Successor

KW - Unit Clause

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-84948970279&partnerID=MN8TOARS

M3 - Chapter

SN - 9783540439318

T3 - Lecture Notes in Computer Science

SP - 260

EP - 274

BT - Automated Deduction - CADE-18

A2 - Voronkov, Andrei

PB - Springer Berlin

CY - Heidelberg

ER -

A New Clausal Class Decidable by Hyperresolution

Abstract

Publication series

Keywords

Other files and links

Fingerprint

Cite this