Effectively Monadic Predicates
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
Abstract
Open-access reader
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
Abstract
Open-access reader
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.
OpenAlex reports 1 citations for this work. Citation counts describe recorded attention and do not establish research quality.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
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.
Key concepts: Decidability, Monadic predicate calculus, Quantifier (linguistics), Automaton, Computer science, Decision problem, Theoretical computer science, Discrete mathematics