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
相关论文
共 71 条
  • [1] Modal languages and bounded fragments of predicate logic
    Andreka, H
    Nemeti, I
    van Benthem, J
    [J]. JOURNAL OF PHILOSOPHICAL LOGIC, 1998, 27 (03) : 217 - 274
  • [2] [Anonymous], 1978, PROC STOC 1978, DOI DOI 10.1145/800133.804361
  • [3] [Anonymous], 1929, Comptes-Rendus du Ler Congress Des Mathematiciens Des Pays Slavs
  • [4] [Anonymous], 1960, Trans. Amer. Math. Soc., DOI DOI 10.1090/S0002-9947-1960-0111704-1
  • [5] [Anonymous], HDB FORMAL LANGUAGES
  • [6] [Anonymous], 1959, Fundamenta Mathematicae
  • [7] [Anonymous], 1997, Perspectives in Mathematical Logic
  • [8] [Anonymous], 1974, COMPLEXITY COMPUTATI
  • [9] [Anonymous], 2006, COMPILERS PRINCIPLES
  • [10] Baaz M., 2001, Handbook of Automated Reasoning, V1, P273
12345678