- 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:combining_fol_models [2012/05/21 19:48] vkuncak |
sav08:combining_fol_models [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 11: | Line 11: | ||

**Proof (using interpolation):** First-order logic has interpolation property, by Craig's interpolation theorem. Suppose we have models for | **Proof (using interpolation):** First-order logic has interpolation property, by Craig's interpolation theorem. Suppose we have models for | ||

$C_1 \cup Ax_1$ and $C_2 \cup Ax_2$, but that there is no model for | $C_1 \cup Ax_1$ and $C_2 \cup Ax_2$, but that there is no model for | ||

- | $C_1 \cup C_2 \cup Ax_1 \cup Ax_2$. By compactness for first-order logic there exists a finite subset that is contradictory. By interpolation there exists an interpolant $I$ that is, say, implied by $C_1 \cup Ax_1$ and contradictory with $C_2 \cup Ax_2$. The interpolant is in the common language, so it contains only equalities. It can be quantified, but over infinite domains quantifiers can be eliminated in a very simple way. So, the result is a disjunction of conjunctions of equalities and disequalities among the common variables. But because $C_1$ and $C_2$ contain a complete atomic type, they either imply or are contradictory with $I$, depending on whether the atomic diagram normal form contains the atomic type present in $C_1,C_2$ or not. Note that $I \cup C_2 \cup Ax_2$ is contradictory since $I$ is interpolant, so each conjunct in its DNF is contradictory. Therefore, $I$ does not have as a disjunct the atomic diagram present in $C_2$ or $C_1$. Then $I$ is contradictory with $C_1$ as well. Since $I$ is a consequence of $C_1 \cup Ax_1$, it follows that $C_1 \cup Ax_1$ is contradictory. But we assumed it is satisfiable. **End** | + | $C_1 \cup C_2 \cup Ax_1 \cup Ax_2$. By compactness for first-order logic there exists a finite subset that is contradictory. By interpolation there exists an interpolant $I$ that is, say, implied by $C_1 \cup Ax_1$ and contradictory with $C_2 \cup Ax_2$. The interpolant is in the common language, so it contains only equalities. It can be quantified, but over infinite domains quantifiers can be eliminated in a very simple way (and in any case, it is a fragment of BAPA that has QE). So, the result is a disjunction of conjunctions of equalities and disequalities among the common variables. But because $C_1$ and $C_2$ contain a complete atomic type, they either imply or are contradictory with $I$, depending on whether the atomic diagram normal form contains the atomic type present in $C_1,C_2$ or not. Note that $I \cup C_2 \cup Ax_2$ is contradictory since $I$ is interpolant, so each conjunct in its DNF is contradictory. Therefore, $I$ does not have as a disjunct the atomic diagram present in $C_2$ or $C_1$. Then $I$ is contradictory with $C_1$ as well. Since $I$ is a consequence of $C_1 \cup Ax_1$, it follows that $C_1 \cup Ax_1$ is contradictory. But we assumed it is satisfiable. **End** |

**Example:** Take formula | **Example:** Take formula | ||

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

x=1 \land f(x)=y \land z=y+y \land f(z)=x \land y \neq x | x=1 \land f(x)=y \land z=y+y \land f(z)=x \land y \neq x | ||

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

If we take a finite model for uninterpreted functions, we cannot merge it with the model for addition. But there is an infinite model for uninterpreted functions as well, and we can merge this model with the model for integers. | If we take a finite model for uninterpreted functions, we cannot merge it with the model for addition. But there is an infinite model for uninterpreted functions as well, and we can merge this model with the model for integers. | ||

Line 60: | Line 60: | ||

In some cases there is no single equality that follows, but only a disjunction can be derived: | In some cases there is no single equality that follows, but only a disjunction can be derived: | ||

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

1 \le x \land x \le 2 \land y = 1 \land z = 2 | 1 \le x \land x \le 2 \land y = 1 \land z = 2 | ||

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

implies $x=y \lor x=z$ but not any other non-trivial equality between variables. We say integer linear arithmetic is a //non-convex theory//. | implies $x=y \lor x=z$ but not any other non-trivial equality between variables. We say integer linear arithmetic is a //non-convex theory//. | ||