2017/04/30 by Margus Veanes, Nikolaj Bjørner, Lev Nachmanson +1 · 3 citations
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #semigroups and automata theory
paper · doi:10.1145/3040488
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.