- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav08:list_of_theories_admitting_qe [2008/04/23 15:28] vkuncak |
sav08:list_of_theories_admitting_qe [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 14: | Line 14: | ||

A language containing arbitrary function symbols and constants. If $GT$ is set of ground terms over ${\cal L}$, we consider the class of interpretations $I = (GT, \alpha)$ where | A language containing arbitrary function symbols and constants. If $GT$ is set of ground terms over ${\cal L}$, we consider the class of interpretations $I = (GT, \alpha)$ where | ||

- | \[ | + | \begin{equation*} |

\alpha(f)(t_1,\ldots,t_n) = | \alpha(f)(t_1,\ldots,t_n) = | ||

- | \] | + | \end{equation*} |

The question of whether terms are unifiable, | The question of whether terms are unifiable, | ||

- | \[ | + | \begin{equation*} |

r(x,f(x,y)) \doteq r(f(a,v),f(f(u,b),f(u,u))) | r(x,f(x,y)) \doteq r(f(a,v),f(f(u,b),f(u,u))) | ||

- | \] | + | \end{equation*} |

becomes the truth value of | becomes the truth value of | ||

- | \[ | + | \begin{equation*} |

\exists x,y,u, v. r(x,f(x,y)) = r(f(a,v),f(f(u,b),f(u,u))) | \exists x,y,u, v. r(x,f(x,y)) = r(f(a,v),f(f(u,b),f(u,u))) | ||

- | \] | + | \end{equation*} |

in this theory. We can express more complex constraints. | in this theory. We can express more complex constraints. | ||

Line 50: | Line 50: | ||

* [[http://theory.stanford.edu/~tingz/papers/jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]] | * [[http://theory.stanford.edu/~tingz/papers/jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]] | ||

+ | |||

===== Products of Structures admiting QE ====== | ===== Products of Structures admiting QE ====== | ||

- | Fefeman-Vaught theorem: if we have decidable theories. | + | Fefeman-Vaught theorem: |

+ | * reduce the truth value of quantified formulas over sequences of elements to truth value of formulas over elements | ||

+ | * the operations on sequences are defined point-wise | ||

+ | More information in references cited here: | ||

* [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]] | * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]] | ||

+ | |||

+ | **Example:** Consider logic that quantifies over pairs of integers and where addition is given by | ||

+ | \begin{equation*} | ||

+ | (x,y) + (u,v) = (x+u,y+v) | ||

+ | \end{equation*} | ||

+ | \begin{equation*} | ||

+ | (x,y) < (u,v) \ \leftrightarrow\ (x < y \land y < v) | ||

+ | \end{equation*} | ||

+ | Formulas in such logic, where variables range over pairs, can be reduced to Presburger arithmetic. | ||

+ | |||

+ | Moreover, such reduction can be done even when variables range over infinite sequences of integers | ||

===== Positive Integers with Multiplication ===== | ===== Positive Integers with Multiplication ===== | ||

Line 62: | Line 77: | ||

Consider prime factor representation of integers: | Consider prime factor representation of integers: | ||

- | \[ | + | \begin{equation*} |

x = \prod_{i=1}^n p_i^{\alpha_i} | x = \prod_{i=1}^n p_i^{\alpha_i} | ||

- | \] | + | \end{equation*} |

where $p_1,p_2,\ldots$ is sequence of prime numbers and $\alpha_i \ge 0$. | where $p_1,p_2,\ldots$ is sequence of prime numbers and $\alpha_i \ge 0$. | ||

Line 84: | Line 99: | ||

Linear arithmetic over rationals ($+$, $\le$, multiplication by rational constants) with operator, for $x \in \mathbb{Q}$, | Linear arithmetic over rationals ($+$, $\le$, multiplication by rational constants) with operator, for $x \in \mathbb{Q}$, | ||

- | \[ | + | \begin{equation*} |

\lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \} | \lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \} | ||

- | \] | + | \end{equation*} |

Observe that this also subsumes Presburger arithmetic. | Observe that this also subsumes Presburger arithmetic. |