Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Monadic Decomposition

Margus Veanes, Nikolaj Bjorner, Lev Nachmanson, and Sergey Bereg

Abstract

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 over a decidable background theory, such as arithmetic and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.

Details

Publication typeInproceedings
Published inCAV'14
URLhttp://www.springerprofessional.de/042---monadic-decomposition/5191358.html
Pages628-645
Volume8559
SeriesLNCS
PublisherSpringer
> Publications > Monadic Decomposition