Maslov’s Class K Revisited

Ullrich Hustadt; R.A. Schmidt

doi:10.1007/3-540-48660-7_12

Maslov’s Class K Revisited

Ullrich Hustadt, R.A. Schmidt

Formal Methods

University of Liverpool

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

Abstract

This paper gives a new treatment of Maslov’s class K in the framework of resolution. More specifically, we show that K and the class DK consisting of disjunction of formulae in K can be decided by a resolution refinement based on liftable orderings. We also discuss relationships to other solvable and unsolvable classes.

Original language	English
Title of host publication	Automated Deduction - CADE-16
Subtitle of host publication	16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings
Editors	Harald Ganzinger
Place of Publication	Heidelberg
Publisher	Springer Berlin
Pages	172-186
Number of pages	15
ISBN (Electronic)	9783540486602
ISBN (Print)	9783540662228
DOIs	https://doi.org/10.1007/3-540-48660-7_12
Publication status	Published - 23 Jun 1999

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1632

Keywords

Modal Logic
Decision Procedure
Function Symbol
Predicate Symbol
Split Component

Access to Document

10.1007/3-540-48660-7_12

Cite this

@inbook{cf3b615693a245d8baa324dddb239748,

title = "Maslov{\textquoteright}s Class K Revisited",

abstract = "This paper gives a new treatment of Maslov{\textquoteright}s class K in the framework of resolution. More specifically, we show that K and the class DK consisting of disjunction of formulae in K can be decided by a resolution refinement based on liftable orderings. We also discuss relationships to other solvable and unsolvable classes.",

keywords = "Modal Logic, Decision Procedure, Function Symbol, Predicate Symbol, Split Component",

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

year = "1999",

month = jun,

day = "23",

doi = "10.1007/3-540-48660-7_12",

language = "English",

isbn = "9783540662228",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin",

pages = "172--186",

editor = "Harald Ganzinger",

booktitle = "Automated Deduction - CADE-16",

address = "Germany",

}

Maslov’s Class K Revisited. / Hustadt, Ullrich; Schmidt, R.A.
Automated Deduction - CADE-16: 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings. ed. / Harald Ganzinger. Heidelberg: Springer Berlin, 1999. p. 172-186 (Lecture Notes in Computer Science; Vol. 1632).

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

TY - CHAP

T1 - Maslov’s Class K Revisited

AU - Hustadt, Ullrich

AU - Schmidt, R.A.

PY - 1999/6/23

Y1 - 1999/6/23

N2 - This paper gives a new treatment of Maslov’s class K in the framework of resolution. More specifically, we show that K and the class DK consisting of disjunction of formulae in K can be decided by a resolution refinement based on liftable orderings. We also discuss relationships to other solvable and unsolvable classes.

AB - This paper gives a new treatment of Maslov’s class K in the framework of resolution. More specifically, we show that K and the class DK consisting of disjunction of formulae in K can be decided by a resolution refinement based on liftable orderings. We also discuss relationships to other solvable and unsolvable classes.

KW - Modal Logic

KW - Decision Procedure

KW - Function Symbol

KW - Predicate Symbol

KW - Split Component

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

U2 - 10.1007/3-540-48660-7_12

DO - 10.1007/3-540-48660-7_12

M3 - Chapter

SN - 9783540662228

T3 - Lecture Notes in Computer Science

SP - 172

EP - 186

BT - Automated Deduction - CADE-16

A2 - Ganzinger, Harald

PB - Springer Berlin

CY - Heidelberg

ER -

Maslov’s Class K Revisited

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Cite this