\usepackagepifont \definecolorfakeaaltobluelRGB00,141,229 \definecoloraaltoblueRGB00,101,189 \definecoloraaltoredRGB237,41,57 \definecolorMyBoxBackgroundrgb0.98,0.98,1.0 \definecolorMyBoxBorderrgb0.90,0.90,1.0 \definecolorbackgroundredrgb1.0,0.98,0.98 \definecolorshadowredrgb1.0,0.90,0.90 \newcommand{\subheading}[1]{\large{\usebeamercolor[fg]{frametitle} #1}} %\newtcbox{\mybox}[1][red]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt} %\newtcbox{\mybox}[1][MyBoxBackground]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt} \newtcolorbox{MyBoxTitled}[1]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=2pt,left=0pt,right=0pt,top=2pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,title=#1,boxrule=1pt} \newtcolorbox{MyBox}[1][]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=0pt,left=2pt,right=0pt,top=0pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,boxrule=1pt,#1} \newenvironment{EqnBox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}\begin{MyBox}[colback=backgroundred!100!black,colframe=shadowred!100!black]}{\end{MyBox}\end{minipage}\end{adjustbox}} \newenvironment{topbox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}}{\end{minipage}\end{adjustbox}} \newcommand{\Blue}[1]{{\color{aaltoblue}#1}} \newcommand{\Red}[1]{{\color{aaltored}#1}} %\newcommand{\Emph}[1]{\emph{\color{aaltoblue}#1}} \newcommand{\Emph}[1]{\emph{\usebeamercolor[fg]{structure} #1}} \newcommand{\TextDef}[1]{{\bf\usebeamercolor[fg]{structure} #1}} \newcommand{\todo}[1]{\textbf{\Red{\Pointer #1}}} \newcommand{\TODO}[1]{\todo{#1}} \newcommand{\Pointer}{\raisebox{-1ex}{\huge\ding{43}}\ } % % Common math definitions % \newcommand{\Set}[1]{\{#1\}} \newcommand{\Setdef}[2]{\{{#1}\mid{#2}\}} \newcommand{\PSet}[1]{\mathcal{P}(#1)} \newcommand{\Pair}[2]{(#1,#2)} \newcommand{\Card}[1]{{\vert{#1}\vert}} \newcommand{\Tuple}[1]{(#1)} \newcommand{\Seq}[1]{[#1]} \newcommand{\bbZ}{\mathbb{Z}} \newcommand{\Ints}{\mathbb{Z}} \newcommand{\Reals}{\mathbb{R}} \newcommand{\bbQ}{\mathbb{Q}} \newcommand{\Rats}{\bbQ} \newcommand{\bbN}{\mathbb{N}} \newcommand{\Nats}{\bbN} \newcommand{\Floor}[1]{\lfloor #1 \rfloor} \newcommand{\Ceil}[1]{\lceil #1 \rceil} \newcommand{\False}{\textsf{F}} \newcommand{\True}{\textsf{T}} \newcommand{\Implies}{\rightarrow} \newcommand{\Iff}{\leftrightarrow} %\newcommand{\Implies}{\Rightarrow} %\newcommand{\Iff}{\Leftrightarrow} \newcommand{\Xor}{\oplus} \newcommand{\Equiv}{\equiv} \newcommand{\Oh}[1]{O(#1)} %\newcommand{\Theta}[1]{\Theta(#1)} \newcommand{\PHP}[2]{\mathrm{php}_{#1,#2}} \newcommand{\PH}[2]{\mathit{x}_{#1,#2}} \newcommand{\NP}{\textbf{NP}} \newcommand{\coNP}{\textbf{co-NP}} \newcommand{\bnfdef}{\mathrel{\textup{::=}}} \newcommand{\bnfor}{\mathrel{\mid}}
\newcommand{\Def}{\mathrel{:=}} \newcommand{\LSF}{\alpha} \newcommand{\RSF}{\beta} \newcommand{\SF}{\phi} \newcommand{\MF}{\gamma} %\newcommand{\Abbrv}{\equiv} \newcommand{\Abbrv}{\Def} \newcommand{\AbbrvEq}{\equiv} \newcommand{\Exists}[2]{\exists{#1}.\,#2} %\newcommand{\E}[3]{\exists{#1{:}#2}.\,#3} \newcommand{\E}[3]{\exists{#1{:}\,#3}} \newcommand{\Forall}[2]{\forall{#1}.\,#2} %\newcommand{\Furall}[3]{\forall{#1{:}#2}.\,#3} %\newcommand{\A}[3]{\forall{#1{:}#2}.\,#3} \newcommand{\A}[3]{\forall{#1{:}\,#3}} \newcommand{\Models}{\models} \newcommand{\NotModels}{\not\models} \newcommand{\Substf}[3]{#1[#2 \mapsto #3]} \newcommand{\Functions}[2]{[#1 \to #2]} \newcommand{\Eq}{\approx} \newcommand{\EqS}[1]{\approx_{#1}} \newcommand{\Neq}{\not\approx} %\newcommand{\Th}{\mathcal{T}} \newcommand{\Th}{T} \newcommand{\ThI}[1]{\Th_{#1}} \newcommand{\Sig}{\Sigma} \newcommand{\SigI}[1]{\Sigma_{#1}} \newcommand{\Interp}{I} %\newcommand{\Interp}{{\mathcal{I}}} \newcommand{\InterpOf}[1]{#1^\Interp} \newcommand{\InterpIOf}[2]{#2^{#1}} \newcommand{\InterpRestr}[1]{\Interp^{#1}} \newcommand{\InterpI}[1]{I_{#1}} %\newcommand{\InterpI}[1]{{\mathcal{I}_{#1}}} %\newcommand{\InterpIOf}[2]{#2^{\InterpI{#1}}} \newcommand{\InterpDom}{D_{\Interp}} \newcommand{\InterpSubst}[2]{\Interp[{#1}\mapsto{#2}]} \newcommand{\ThModels}{\mathrel{\models_{\Th}}} \newcommand{\ThIModels}[1]{\mathrel{\models_{\ThI{#1}}}} % Example interpretations \newcommand{\IInts}{\InterpI{\textrm{ints}}} \newcommand{\IIntsOf}[1]{\InterpIOf{\IInts}{#1}} \newcommand{\IMods}{\InterpI{\textrm{mod7}}} \newcommand{\IModsOf}[1]{\InterpIOf{\IMods}{#1}} \newcommand{\ISilly}{\InterpI{\textrm{silly}}} \newcommand{\ISillyOf}[1]{\InterpIOf{\ISilly}{#1}} %\newcommand{\El}[1]{\textup{e}_{#1}} \newcommand{\ElemI}{\textup{\ding{40}}} \newcommand{\ElemII}{\textup{\ding{41}}} \newcommand{\ElemIII}{\textup{\ding{46}}} \newcommand{\ElemA}{\circ} \newcommand{\ElemB}{\bullet} \newcommand{\AxiomMarg}[1]{\makebox{}\hfill(\Blue{#1})} \newcommand{\Comment}[1]{\makebox{}\hfill\Blue{#1}} \newcommand{\DLZ}{\mathit{DL}(\bbZ)} \newcommand{\DLQ}{\mathit{DL}(\bbQ)} \newcommand{\EUF}{\mathit{EUF}} \newcommand{\TEUF}{\ThI{\mathit{EUF}}} \newcommand{\LIA}{\mathit{LIA}} \newcommand{\TLIA}{\ThI{\mathit{LIA}}} \newcommand{\TNRA}{\ThI{\mathit{NRA}}} \newcommand{\TNIA}{\ThI{\mathit{NIA}}} \newcommand{\LRA}{\mathit{LRA}} \newcommand{\TLRA}{\ThI{\mathit{LRA}}} \newcommand{\IDL}{\mathit{IDL}} \newcommand{\RDL}{\mathit{RDL}} \newcommand{\EUFModels}{\mathrel{\models_{\TEUF}}} \newcommand{\EUFModelsNot}{\mathrel{{\not\models}_{\TEUF}}} \newcommand{\LIAModels}{\mathrel{\models_{\LIA}}} \newcommand{\LIANotModels}{\mathrel{\not\models_{\LIA}}} \newcommand{\LIAEntails}{\mathrel{\models_{\LIA}}} \newcommand{\IDLEntails}{\mathrel{\models_{\IDL}}} \newcommand{\NIAModels}{\mathrel{\models_{\TNIA}}} \newcommand{\Div}[2]{{{#1}\mid{#2}}} \newcommand{\Sort}{s} \newcommand{\SortI}[1]{s_{#1}} \newcommand{\Sorts}{S} \newcommand{\Func}{f} \newcommand{\Funcs}{F} \newcommand{\Pred}{p} \newcommand{\Preds}{P} \newcommand{\SortName}[1]{\textsf{#1}} \newcommand{\Var}{x} \newcommand{\Vars}{X} \newcommand{\BVar}{a} \newcommand{\BVars}{\mathcal{B}} \newcommand{\Val}{v} \newcommand{\DomOf}[1]{D_{#1}} \newcommand{\Term}{t} \newcommand{\TermI}[1]{t_{#1}} \newcommand{\TermP}[1]{t'} \newcommand{\Atom}{A} % % EUF % \newcommand{\UFEq}{\equiv} \newcommand{\UFEqP}{\mathrel{\equiv'}} \newcommand{\UFEqNot}{\not\equiv} \newcommand{\UFNeq}{\not\equiv} % % Arithmetics % \newcommand{\IntsSort}{\textrm{Int}} \newcommand{\IntsSig}{\SigI{\textrm{Int}}} \newcommand{\RealsSort}{\textrm{Real}} \newcommand{\Mul}{\mathbin{*}} % % Arrays % \newcommand{\IndexSort}{\SortName{idx}} %\newcommand{\IndexSort}{\SortName{index}} \newcommand{\ElemSort}{\SortName{elem}} %\newcommand{\ArraySort}{\SortName{array}} \newcommand{\ArraySort}{\SortName{arr}} \newcommand{\ArrSig}{\Sigma_{\mathit{arrays}}} \newcommand{\ArrE}[1]{\textrm{a}_{#1}} \newcommand{\TArrays}{\ThI{\mathit{arrays}}} \newcommand{\TArraysExt}{\ThI{\mathit{arrays}}^{=}} \newcommand{\ArrModels}{\mathrel{{\models_\mathit{arrays}}}} % % Theories of Lisp-like lists % \newcommand{\ThCons}{\ThI{\textrm{cons}}} \newcommand{\ThConsAcyclic}{\ThI{\textrm{cons+}}} \newcommand{\SigCons}{\SigI{\textrm{cons}}} \newcommand{\Cons}{\FuncName{cons}} \newcommand{\Car}{\FuncName{car}} \newcommand{\Cdr}{\FuncName{cdr}} \newcommand{\LAtom}{\PredName{atom}} % Sorted version additions \newcommand{\ListSort}{\SortName{list}} \newcommand{\Nil}{\FuncName{nil}} \newcommand{\Length}{\FuncName{length}} \newcommand{\BVT}{\ThI{\mathsf{BV}}} \newcommand{\BVSig}{\SigI{\mathsf{BV}}} \newcommand{\BVS}[1]{\SortName{[}#1\SortName{]}} %\newcommand{\BVS}[1]{[{#1}]} \newcommand{\BVAdd}[1]{\mathbin{{+}_{\BVS{#1}}}} \newcommand{\BVLE}[1]{\mathbin{{\le}_{\BVS{#1}}}} \newcommand{\BVGE}[1]{\mathbin{{\ge}_{\BVS{#1}}}} \newcommand{\BVSL}[1]{\mathbin{{\ll}_{\BVS{#1}}}} \newcommand{\BVTermB}[1]{\hat{t}_{(#1)}} %\newcommand{\BVTermBI}[2]{\hat{t}_{#1}^{(#2)}} \newcommand{\BVAtom}{\hat{A}} \newcommand{\BVXB}[1]{\hat{x}_{(#1)}} \newcommand{\BVYB}[1]{\hat{y}_{(#1)}} \newcommand{\BVVar}[1]{\hat{x}_{(#1)}} % SMTLIB logics \newcommand{\SMTLIBLogic}[1]{\textrm{#1}} \newcommand{\QFUF}{\SMTLIBLogic{QF\_UF}} \newcommand{\QFLIA}{\SMTLIBLogic{QF\_LIA}} \newcommand{\QFUFLRA}{\SMTLIBLogic{QF\_UFLRA}} \newcommand{\SMTLIBLIA}{\SMTLIBLogic{LIA}} \newcommand{\CG}[1]{G_{#1}} \newcommand{\DiffEdge}[1]{\overset{#1}{\longrightarrow}} \newcommand{\FuncName}[1]{\textsf{#1}} \newcommand{\PredName}[1]{\textsf{#1}} \newcommand{\ReadF}{\FuncName{read}} \newcommand{\Read}[2]{\ReadF(#1,#2)} \newcommand{\WriteF}{\FuncName{write}} \newcommand{\Write}[3]{\WriteF(#1,#2,#3)} \newcommand{\Abs}[1]{\alpha_{#1}} \newcommand{\Expl}[1]{\textit{explain}(#1)} \newcommand{\SMTAssertF}{\textsf{assert}} \newcommand{\SMTAssert}[1]{\SMTAssertF(#1)} \newcommand{\UFRoot}{\textit{parent}} \newcommand{\UFRootOf}[1]{{#1}.\UFRoot} \newcommand{\UFRank}{\textit{rank}} \newcommand{\UFRankOf}[1]{{#1}.\UFRank} \newcommand{\UFFind}[1]{\textsf{find}(#1)} \newcommand{\UFMerge}[2]{\textsf{merge}(#1,#2)} \newcommand{\CCPending}{\textit{pending}} % % Theory solver interface % \newcommand{\TSinit}[1]{\mathop{init}(#1)} \newcommand{\TSassert}[1]{\mathop{assert}(#1)} \newcommand{\TSretract}{\mathop{retract}()} \newcommand{\TSisSat}{\mathop{isSat}()} \newcommand{\TSgetModel}{\mathop{getModel}()} \newcommand{\TSgetImplied}{\mathop{getImplied}()} \newcommand{\TSexplain}[1]{\mathop{explain}(#1)} \newcommand{\VarsOf}[1]{\mathop{vars}(#1)} \newcommand{\Dist}[1]{\mathit{dist}(#1)} %\newcommand{\Dist}[1]{\mathit{dist}(#1)} % % Nelson-Oppen % \newcommand{\TComb}{\cup} \newcommand{\NOShared}[1]{\mathop{\textrm{shared}}(#1)} \newcommand{\NOPart}{P} \newcommand{\NOPartI}[1]{P_{#1}} %\newcommand{\NOEq}{\mathrel{\approx}} %\newcommand{\NOEqNot}{\mathrel{\not\approx}} \newcommand{\NOEq}{\mathrel{{\equiv_{P}}}} %\newcommand{\NOEq}{\stackrel{\NOPart}{\equiv}} \newcommand{\NOEqNot}{\mathrel{\not\equiv_{\NOPart}}} %\newcommand{\NOEqNot}{\stackrel{\NOPart}{\not\equiv}} \newcommand{\NOArr}{\mathop{arr}(P)} \newcommand{\NOArrI}[1]{\mathop{arr}(P_{#1})} % % Example formulas in Nelson-Oppen part % \newcommand{\NOF}{\phi} %\newcommand{\NOFA}{\phi_1} %\newcommand{\NOFB}{\phi_2} %\newcommand{\NOTA}{\ThI{1}} %\newcommand{\NOTB}{\ThI{2}} \newcommand{\NOFEUF}{\phi_\mathit{EUF}} \newcommand{\NOFLIA}{\phi_\mathit{LIA}} \newcommand{\NOFLRA}{\phi_\mathit{LRA}} \newcommand{\NOFCons}{\phi_\textup{cons}} %\newcommand{\Asgn}{\mathrel{:=}} \newcommand{\Asgn}{\mathrel{\leftarrow}} %\newcommand{\Engl}[1]{(engl.\ #1)} \newcommand{\Ack}[1]{\mathop{ack}(#1)} \newcommand{\VVar}[1]{v_{#1}} \newcommand{\FVar}[2]{{#1}_{#2}} \newcommand{\PVar}[2]{{#1}_{#2}} \newcommand{\Flat}{{\phi_\textrm{flat}}} \newcommand{\Cong}{{\phi_\textrm{cong}}} \newcommand{\In}{\mathit{in}} \newcommand{\Out}{\mathit{out}} \newcommand{\SubType}{\FuncName{subtype}} % % Fourier-Motzkin elimination % \newcommand{\FM}{\phi} \newcommand{\FMup}{\phi^\textrm{up}} \newcommand{\FMlo}{\phi^\textrm{low}} %\newcommand{\FMup}{\phi^{\le}} %\newcommand{\FMlo}{\phi^{\ge}} \newcommand{\FMindep}{\phi^{\ast}} \newcommand{\Nup}{n^\textrm{up}} \newcommand{\Nlo}{n^\textrm{low}} %\newcommand{\Nup}{n^{\le}} %\newcommand{\Nlo}{n^{\ge}} \newcommand{\Rup}[1]{A^\textrm{up}_{#1}} \newcommand{\Rlo}[1]{A^\textrm{low}_{#1}} %\newcommand{\Rup}[1]{A^{\le}_{#1}} %\newcommand{\Rlo}[1]{A^{\ge}_{#1}} %\newcommand{\FMless}{\mathrel{\triangleleft}} %\newcommand{\FMmore}{\mathrel{\triangleright}} \newcommand{\ProblemName}[1]{\textup{#1}} \newcommand{\ATM}{A_\textup{TM}} \newcommand{\PCP}{\ProblemName{PCP}} \newcommand{\MPCP}{\ProblemName{MPCP}} \newcommand{\PCPAst}{\star} \newcommand{\Eps}{\varepsilon} \newcommand{\List}[1]{[#1]} \newcommand{\Strings}[1]{\{#1\}^\star} \newcommand{\StringsOver}[1]{{#1}^\star} \newcommand{\SigmaStrings}{\Sigma^\star} \newcommand{\GammaStrings}{\Gamma^\star} \newcommand{\Complement}[1]{\overline{#1}} % % SSA example % \newcommand{\In}{\mathit{in}} \newcommand{\Out}{\mathit{out}} % % % \newcommand{\DA}{♠} \newcommand{\DB}{♥} \newcommand{\DC}{♦} \newcommand{\DD}{♣}

Quantified Formulas

So far we have concentrated on quantifier-free satisfiability. But how about quantifiers? They can be used to express, e.g., verification conditions such as \A{x_1}{\ElemSort}{\A{x_2}{\ElemSort}{\A{x_3}{\ElemSort}{\SubType(x_1,x_2)\land\SubType(x_2,x_3)\Implies\SubType(x_1,x_3)}}} Handling quantifiers in SMT is a long-standing challenge and an ongoing research topic. Some SMT solvers have (possibly incomplete) algorithms for handling quantifiers.

Quantifier elimination

Some theories allow us to get rid of the quantifiers, meaning that we can get an equivalent formula that has no quantifiers. Formally, a \Sig -theory \Th admits quantifier elimination if there is an algorithm that, given a \Sig -formula F , returns a quantifier-free \Sig -formula G that is \Th -equivalent to F (meaning that each interpretation \Interp is a \Th -model of F iff it is a \Th -model of G ).

Example

The theory of linear arithmetic over reals, \TLRA , admits quantifier elimination.

Eliminating y from \begin{array}{rl}\A{x}{\RealsSort}{\E{y}{\RealsSort}{}}&({x-y \ge 1}\land{-x-2y \le -1}\land{-2x-y\ge-8}) \lor\\\\& ({x-y \le 2}\land{-x-2y \ge 1})\end{array} we get \A{x}{\RealsSort}{({1 \le x}\land{x \le 5}) \lor (x \le 1)} and then \False after eliminating x .

The figure below shows the inequalities as lines and the areas described by the first conjunction in blue and the second one in green. Elimination of y results on the projection of these areas on the x-axis.

_images/qe-ex-1.png

Some theories do not admit quantifier elimination but small extensions do:

Example

The theory of linear arithmetic over integers \TLIA does not admit quantifier elimination. For instance, the formula \E{x}{\IntsSort}{2x=y} does not have a \TLIA -equivalent quantifier-free formula.

If we augment the theory \TLIA with the divisibility predicate \Div{d}{n} evaluating to true whenever n is divisible by d , the resulting theory admits quantifier elimination. As an example, a quantifier-free version of \E{x}{\IntsSort}{2x=y} is \Div{2}{y} .

For further discussion, see Section 7.1 in Aaron Bradley and Zohar Manna: The Calculus of Computation, Springer, 2007

Fourier-Motzkin elimination

The Fourier–Motzkin elimination method is a quantifier elimination method for linear arithmetic over reals. It is conceptually rather simple but may require lots of memory in practise. The idea is to eliminate quantifiers one-by-one, starting from the innermost quantifier. It only works for conjunctions of atoms and, therefore, the formula must be translated into DNF. Furthermore, it can only eliminate existential quantifiers but universal quantifiers can be handled by using the equivalence {\forall x: \phi} \Equiv {\neg \exists x: \neg \phi} to eliminate \forall x: \phi as follows:

  1. negate the formula \phi and translate the result to DNF,

  2. apply the Fourier-Motzkin method to each disjunct, and

  3. negate the disjunction of the results.

Eliminating an existentially quantified variable can be done as follows. For simplicity, we only consider inequalities \le and \ge . Assume a conjunction \FM of linear inequalities over n variables x_1,…,x_n and a variable to be eliminated, say x_1 . The inequalities in \FM can be rewritten into \FMup \land \FMlo \land \FMindep, where

  • \FMlo contains the \Nlo inequalities of the form b_l + \sum_{j=2}^{n} a_{j,l} x_j \le x_1 in \FM . For each 1 \le l \le \Nlo , let \Rlo{l}(x_2,…,x_n) = b_l + \sum_{j=2}^{n} a_{j,l} x_j .

  • \FMup contains the \Nup inequalities of the form x_1 \le b_k + \sum_{j=2}^{n} a_{j,k} x_j in \FM . For each 1 \le k \le \Nup , let with \Rup{k}(x_2,…,x_n) = b_k + \sum_{j=2}^{n} a_{j,k} x_j .

  • \FMindep is the conjunction of the inequalities in \FM that do not involve x_1 .

The conjunction \FMup \land \FMlo \land \FMindep is satisfiable if and only if there exists a real-valued assignment on \Set{x_2,…,x_n} that

  1. evaluates \FMindep to true and

  2. there is a value on x_1 so that \Rlo{l}(x_2,…,x_n) \le x \le \Rup{k}(x_2,…,x_n) holds each 1 \le l \le \Nlo and 1 \le k \le \Nup

Thus \FMup \land \FMlo \land \FMindep over the variables x_1,…,x_n is satisfiable if and only if \FMindep \land \bigwedge_{1 \le l \le \Nlo, 1 \le k \le \Nup}{\Rlo{l}(x_2,…,x_n) \le \Rup{k}(x_2,…,x_n)} over the variables x_2,…,x_n is satisfiable. The method above is easy to generalize for strict inequalities as well. The elimination method has double-exponential worst-case complexity when eliminating all the variables in a formula.

Example

Consider the formula (x-y \ge 1)\land(-x-2y \le -1)\land(-2x-y\ge-8) and eliminate y . Now

  • \FMlo \Def (-0.5x+0.5 \le y) ,

  • \FMup \Def (y \le x-1) \land (y \le -2x+8) and

  • \FMindep \Def \True

Thus the resulting formula is (-0.5x+0.5 \le x-1) \land (-0.5x+0.5 \le -2x+8) \land \True that, when simplified, is equivalent to (x \ge 1) \land (x \le 5)

Example

Consider the quantified linear arithmetic over reals formula \begin{array}{rl}\A{x}{\RealsSort}{\E{y}{\RealsSort}{}}&({x-y \ge 1}\land{-x-2y \le -1}\land{-2x-y\ge-8}) \lor\\\\& ({x-y \le 2}\land{-x-2y \ge 1})\end{array} The formula is already in DNF. Eliminating y from the formula, we get \A{x}{\RealsSort}{({1 \le x}\land{x \le 5}) \lor (x \le 1)}

Negating, we get {({1 > x}\lor{x > 5}) \land (x > 1)} , which is ({1 > x} \land {x > 1}) \lor ({x > 5} \land {x > 1}) in DNF.

Simplifying, we get {x > 5} .

Eliminating x we get \E{x}{\RealsSort}{x > 5} = \True and thus \A{x}{\RealsSort}{({1 \le x}\land{x \le 5}) \lor (x \le 1)} = \neg\True = \False .

Other approaches

Solving quantified formulas in the SMT context is an ongoing research topic. One approach used in some current solvers is “quantifier instantiation”

and also search-based methods start to appear