- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:atomic_diagram_normal_form [2009/05/13 10:43] vkuncak |
sav08:atomic_diagram_normal_form [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 7: | Line 7: | ||

By introducing fresh variables, each conjunction of literals can be represented as an equisatisfiable conjunction of only "flat literals", which are flat atomic formulas or their negation, where flat atomic formula is | By introducing fresh variables, each conjunction of literals can be represented as an equisatisfiable conjunction of only "flat literals", which are flat atomic formulas or their negation, where flat atomic formula is | ||

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

R(y_1,\ldots,y_n) | R(y_1,\ldots,y_n) | ||

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

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

x = y | x = y | ||

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

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

x = f(y_1,\ldots,y_n) | x = f(y_1,\ldots,y_n) | ||

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

We call this "flat form" of the conjunction of literals. (We can also eliminate $x \neq f(y_1,\ldots,y_n)$ if needed.) | We call this "flat form" of the conjunction of literals. (We can also eliminate $x \neq f(y_1,\ldots,y_n)$ if needed.) | ||

Rewrite rule that describes this transformation: | Rewrite rule that describes this transformation: | ||

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

C[t] \ \ \leadsto \ \ (x=t) \land C[x] | C[t] \ \ \leadsto \ \ (x=t) \land C[x] | ||

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

**Example:** Represent $f(x)+y < z$ as | **Example:** Represent $f(x)+y < z$ as | ||

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

x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z | x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z | ||

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

Line 62: | Line 62: | ||

Note: if we simply guess all possible conjunctions of literals and negations, some of them will be unsatisfiable in the theory. Those are useless and we should eliminate them. For example, if we consider equality literals, then | Note: if we simply guess all possible conjunctions of literals and negations, some of them will be unsatisfiable in the theory. Those are useless and we should eliminate them. For example, if we consider equality literals, then | ||

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

x \neq z \land y = z \land x = y | x \neq z \land y = z \land x = y | ||

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

is unsatisfiable. Only those conjunctions of equality literals can be satisfiable that correspond to an equivalence relations on variables. Such conjunction of literals that corresponds to an equivalence relation is called **arrangement** in the context of combination techniques. | is unsatisfiable. Only those conjunctions of equality literals can be satisfiable that correspond to an equivalence relations on variables. Such conjunction of literals that corresponds to an equivalence relation is called **arrangement** in the context of combination techniques. | ||

Line 78: | Line 78: | ||

For example, if we have only equality symbol, each partition of the set of variables gives one satisfiable formula (asserting that elements in same partition are equal, in different partitions disequal). Partition $\{\{x,y\},\{z\}\}$ gives formula | For example, if we have only equality symbol, each partition of the set of variables gives one satisfiable formula (asserting that elements in same partition are equal, in different partitions disequal). Partition $\{\{x,y\},\{z\}\}$ gives formula | ||

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

x = y \land x \neq z | x = y \land x \neq z | ||

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

or, if we include all atomic formulas: | or, if we include all atomic formulas: | ||

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

x = y \land y = x \land | x = y \land y = x \land | ||

x \neq z \land z \neq x \land y \neq z \land z \neq y \land | x \neq z \land z \neq x \land y \neq z \land z \neq y \land | ||

x = x \land y = y \land z=z | x = x \land y = y \land z=z | ||

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

+ | The number of partitions is given by [[wp>Bell number]]s. | ||