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 条

[51] Lou van den Dries, 1998, TAME TOPOLOGY O MINI
[52] On possibilities in relative calculus
Lowenheim, L
[J]. MATHEMATISCHE ANNALEN, 1915, 76 : 447 - 470
[53] Malcev AI., 1971, The metamathematics of algebraic systems, collected papers: 19361967
[54] Data-Parallel Finite-State Machines
Mytkowicz, Todd
Musuvathi, Madanlal
Schulte, Wolfram
[J]. ACM SIGPLAN NOTICES, 2014, 49 (04) : 529 - 541
[55] FAST DECISION PROCEDURES BASED ON CONGRUENCE CLOSURE
NELSON, G
OPPEN, DC
[J]. JOURNAL OF THE ACM, 1980, 27 (02) : 356 - 364
[56] Nelson G., 1979, ACM Transactions on Programming Languages and Systems, V1, P245, DOI 10.1145/357073.357079
[57] Niehren J, 2005, LECT NOTES COMPUT SC, V3774, P217
[58] Nielson F., 2010, Principles of Program Analysis
[59] Nipkow T, 2008, LECT NOTES ARTIF INT, V5195, P18, DOI 10.1007/978-3-540-71070-7_3
[60] TRANSDUCTION OF CHOMSKY LANGUAGES
NIVAT, M
[J]. ANNALES DE L INSTITUT FOURIER, 1968, 18 (01) : 339 - &

← 1 2 3 4 5 6 7 8 →