Monadic Decomposition

被引：7
|
作者：
Veanes, Margus [1 ]
Bjorner, Nikolaj [1 ]
Nachmanson, Lev [1 ]
Bereg, Sergey [2 ]
机构：
[1] Microsoft Res, One Microsoft Way, Redmond, WA 98905 USA
[2] Univ Texas Dallas, 800 West Campbell Rd, Richardson, TX 75080 USA
来源：
JOURNAL OF THE ACM | 2017年 / 64卷 / 02期
关键词：
Symbolic automata; variable independence; satisfiability modulo theories; monadic logic; DECIDABILITY; LANGUAGES;
D O I：
10.1145/3040488
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier-free formulas whose satisfiability is decidable, such as linear arithmetic. Here we develop a semidecision procedure for extracting a monadic decomposition of a formula when it exists.
引用
收藏
页数：28
相关论文
共 50 条
  • [1] Monadic Decomposition
    Veanes, Margus
    Bjorner, Nikolaj
    Nachmanson, Lev
    Bereg, Sergey
    COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 628 - 645
  • [2] Monadic vs adjoint decomposition
    Ardizzoni, Alessandro
    Menini, Claudia
    JOURNAL OF PURE AND APPLIED ALGEBRA, 2022, 226 (08)
  • [3] Monadic Decomposition in Integer Linear Arithmetic
    Hague, Matthew
    Lin, Anthony W.
    Rummer, Philipp
    Wu, Zhilin
    AUTOMATED REASONING, PT I, 2020, 12166 : 122 - 140
  • [4] Restricted Lie Algebras via Monadic Decomposition
    Ardizzoni, Alessandro
    Goyvaerts, Isar
    Menini, Claudia
    ALGEBRAS AND REPRESENTATION THEORY, 2018, 21 (04) : 703 - 716
  • [5] Milnor-Moore categories and monadic decomposition
    Ardizzoni, Alessandro
    Menini, Claudia
    JOURNAL OF ALGEBRA, 2016, 448 : 488 - 563
  • [6] Restricted Lie Algebras via Monadic Decomposition
    Alessandro Ardizzoni
    Isar Goyvaerts
    Claudia Menini
    Algebras and Representation Theory, 2018, 21 : 703 - 716
  • [7] Learning Union of Integer Hypercubes with Queries (with Applications to Monadic Decomposition)
    Markgraf, Oliver
    Stan, Daniel
    Lin, Anthony W.
    COMPUTER AIDED VERIFICATION, PT II, CAV 2021, 2021, 12760 : 243 - 265
  • [8] MONADIC COMPLETION OF MONADIC RING
    RIBEYRE, S
    COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES SERIE A, 1971, 273 (20): : 877 - &
  • [9] On Monadic Theories of Monadic Predicates
    Thomas, Wolfgang
    FIELDS OF LOGIC AND COMPUTATION: ESSAYS DEDICATED TO YURI GUREVICH ON THE OCCASION OF HIS 70TH BIRTHDAY, 2010, 6300 : 615 - 626
  • [10] The modular decomposition of countable graphs:: Constructions in monadic second-order logic
    Courcelle, B
    Delhommé, C
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2005, 3634 : 325 - +
12345