4 - Presburger arithmetic

Question 1

how to construct prefburguer automata

Answer 1

same ideia as buchi II:
solution space is the set of accepting values
Encode values as lsbf
Create normal representation [a][x] q’ := floor(1/2 (q - [a]*[bit]) )

this formula is derived from:
word w' encodes [c']
word [bit]w' encodes 2[c'] + [bit] (shift right)
[c'] is accepted from q' 
iff 
2 [c'] + [bit] accepted from q
to satisfy state q we need
[a][c'] <= q
 because then it will accept [0], or epsilon

Question 2

quantifier elimination result

Answer 2

The interest in ∃PA is that satisability has a low complexity

know the steps of proof!!

Here, we want to remove the quantifiers of a prefburger formula ∃x|φ(x,[y]) to create φ(x,[y]), which is wuantifier free

*Step 1: Normalize formula
Transform φ(x,[y]) into negation normal form (NNF)
Eliminate negation
Compute DNF:
nx ? u- t where ? ∈ {=, =m, }
isolate x in each atomic subformula of the DNF

*Step 2: Uniformize and eliminate coefficient on x
Compute least common multiple of coefficients:
p = lcm(n1,…nn)
transform formulas so that coefficient of x is p
nx ? u - t iff
px ? (p/n)u - (p/n)t
for modulo:
nx =m u-t iff
px =((p/n)m) (p/n)u - (p/n)t
replace px by new variable y and add y =p 0
px ? u’ - t’
replaced by
u = u’ - t’
^ y =p 0

*Step 3: Eliminate y
*Step 3a: Special case: There is = on y
y = u’ - t’ : since y >= 0, this becomes:
t’ n)
replace formula with conjunction M

Question 3

talk about congruences

Answer 3

modulus, recorring pattern, important on step 3