- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:herbrand_model_for_an_example [2009/05/14 12:30] vkuncak |
sav08:herbrand_model_for_an_example [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 1: | Line 1: | ||

====== Herbrand Model and Unsat Proof for an Example ====== | ====== Herbrand Model and Unsat Proof for an Example ====== | ||

+ | |||

+ | [[wp>Herbrand]] | ||

We will look at the language ${\cal L} = \{P, R, a, f\}$ where | We will look at the language ${\cal L} = \{P, R, a, f\}$ where | ||

Line 8: | Line 10: | ||

Consider this formula in ${\cal L}$: | Consider this formula in ${\cal L}$: | ||

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

\begin{array}{l@{}l} | \begin{array}{l@{}l} | ||

& (\forall x. \exists y.\ R(x,y))\ \land \\ | & (\forall x. \exists y.\ R(x,y))\ \land \\ | ||

Line 15: | Line 17: | ||

& \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) | & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) | ||

\end{array} | \end{array} | ||

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

We are interested in checking the //validity// of this formula (is it true in all interpretations). We will check the //satisfiability// of the negation of this formula (does it have a model): | We are interested in checking the //validity// of this formula (is it true in all interpretations). We will check the //satisfiability// of the negation of this formula (does it have a model): | ||

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

\begin{array}{l@{}l} | \begin{array}{l@{}l} | ||

\lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ | \lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ | ||

Line 24: | Line 26: | ||

& \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg) | & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg) | ||

\end{array} | \end{array} | ||

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

Parsing the formula. | Parsing the formula. |