Differences

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

--- sav08:list_of_theories_admitting_qe [2008/04/23 15:28]
vkuncak
+++ sav08:list_of_theories_admitting_qe [2009/04/22 10:28]
vkuncak
@@ Line 50: / Line 50: @@
   * [[http://theory.stanford.edu/~tingz/papers/jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]]
 ===== 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]]
+**Example:** Consider logic that quantifies over pairs of integers and where addition is given by
+\[
+   (x,y) + (u,v) = (x+u,y+v)
+\]
+\[
+   (x,y) < (u,v) \ \leftrightarrow\  (x < y \land y < v)
+\]
+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 =====