Mark Reynolds

Synthesis for monadic logic over the reals

We say that a first-order monadic logic of order (FOMLO) sentence is satisfiable over the reals if there is some valuation for the monadic predicates which makes the formula true. Burgess and Gurevich showed that satisfiability for this logic is decidable. They built on pioneering work by Lauchli and Leonard who, in showing a similar result for linear orders in general, had presented some basic operations for the compositional building of monadic linear structures.

We look at some recent work in using these basic operations to give a synthesis result. That is, we present an algorithm which given a FOMLO sentence which is satisfiable over the reals, outputs a specific finite description of a model.