@inproceedings{veanes2014monadic, author = {Veanes, Margus and Bjørner, Nikolaj and Nachmanson, Lev and Bereg, Sergey}, title = {Monadic Decomposition}, series = {LNCS}, booktitle = {CAV'14}, year = {2014}, month = {July}, 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.}, publisher = {Springer}, url = {http://approjects.co.za/?big=en-us/research/publication/monadic-decomposition/}, pages = {628-645}, volume = {8559}, edition = {CAV'14}, }