Buchi arithmetic meaning

85 Views Asked by At

I am studying this article. But I have trouble with understanding the Buchi arithmetic. It says in section IV:

... Formulas in this fragment generalise classical integer programming and are of the form $$ \mathbf{A} \boldsymbol{x}=\boldsymbol{c} \wedge \bigwedge_{i \in I} V_{p}\left(x_{i}\right)=y_{i} $$

But I don't understand what does it mean by $ \mathbf{A} \boldsymbol{x}=\boldsymbol{c} \wedge \bigwedge_{i \in I} V_{p}\left(x_{i}\right)=y_{i} $. I know that the goal is to finding $\boldsymbol{x}$ such that was an answer for previous equation. But my question is about the meaning of $\boldsymbol{c} \wedge \bigwedge_{i \in I} V_{p}\left(x_{i}\right)=y_{i}$. According to the previous sections of the article $\boldsymbol{c}$ is a vector and I want to know what does wedge symbol mean in this case?

In addition, I want to know, as $V_{p}\left(x_{i}\right)$ is an integer, is the big wedge notation here a bitwise and or something else?

As It is the first time I have studied this kind of material, my question may seem naive. However, I appreciate any help containing some references about Buchi arithmetic.

1

There are 1 best solutions below

0
On BEST ANSWER

I think OP is misinterpreting where the implicit parentheses are in the formula

$$\mathbf{A} \boldsymbol{x}=\boldsymbol{c} \wedge \bigwedge_{i \in I} V_{p}\left(x_{i}\right)=y_{i}.$$

This formula means

$$\Big(\mathbf{A} \boldsymbol{x}=\boldsymbol{c}\Big) \;\wedge\;\Big( \bigwedge_{i \in I} \big(V_{p}\left(x_{i}\right)=y_{i}\big)\Big),$$

and, if we write $I = \{i_1, i_2, \dots, i_n \},$ the formula above expands to

$$\Big(\mathbf{A} \boldsymbol{x}=\boldsymbol{c}\Big) \;\wedge\; \Big(V_{p}\left(x_{i_1}\right)=y_{i_1}\Big) \;\wedge\; \Big(V_{p}\left(x_{i_2}\right)=y_{i_2}\Big) \;\wedge\; \dots \;\wedge\; \Big(V_{p}\left(x_{i_n}\right)=y_{i_n}\Big).$$

The big wedge is just a shorthand way of writing a conjunction with $\mid I \mid$ subformulas (indexed by $i\in I$).

So the components of the big wedge are the formulas $\big(V_{p}\left(x_{i}\right)=y_{i}\big),$ not the integers $V_{p}\left(x_{i}\right).$ (Overall, the big wedge is a conjunction of formulas, not some bitwise operation applied to integers.)