A modified completeness theorem of KAT and decidability of term reducibility

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

1 被引用数 (Scopus)

抄録

Kleene algebra with tests (KAT) was introduced by Kozen as an extension of Kleene algebra (KA). The decidability of equational formulas p = q and Horn formulas ∧ipi = qi → p = q in KAT has been studied so far by several researchers. Continuing this line of research, this paper studies the decidability of existentially quantified equational formulas ∃q ∈ P. (p = q) in KAT, where P is a fixed collection of KAT terms. A new completeness theorem of KAT is proved, and via the completeness theorem, the decision problem of ∃q ∈ P. (p = q) is reduced to a certain membership problem of regular languages, to which a pseudo-identity- based decision method is applicable. Based on this reduction, an instance of the problem is studied and shown to be decidable.

本文言語英語
ホスト出版物のタイトルRelational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings
出版社Springer Verlag
ページ83-100
ページ数18
ISBN(印刷版)9783319062501
DOI
出版ステータス出版済み - 2014
外部発表はい
イベント14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014 - Marienstatt, ドイツ
継続期間: 4 28 20145 1 2014

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
8428 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

会議

会議14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014
国/地域ドイツ
CityMarienstatt
Period4/28/145/1/14

All Science Journal Classification (ASJC) codes

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「A modified completeness theorem of KAT and decidability of term reducibility」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル