Differences

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

--- sav08:analyses_based_on_formulas [2009/04/08 10:37]
vkuncak
+++ sav08:analyses_based_on_formulas [2009/04/08 10:44]
vkuncak
@@ Line 14: / Line 14: @@
 \]
 In general, a logic that can represent exact least upper bounds needs to express the conditions such as "there exists a sequence of statements that produces the given state".
@@ Line 43: / Line 44: @@
 Why are there no infinite chains when using such $N$ ?
-To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set).
+To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set):
+\[
+\begin{array}{l}
+   N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\
+\ \ \   \bigwedge (conseq(\{C_1, \ldots, C_n \}) \cap conseq(\{D_1, \ldots, D_m\}))
+\end{array}
+\]
+where
+\[
+    conseq(S) = \{ F \in U.\ \ (S \rightarrow F) \mbox{ is valid } \}
+\]
+where $U$ is some class of useful formulas.
 === References ===
@@ Line 95: / Line 107: @@
 If there is no solution, there is no invariant **of that particular template form**.
-Note: for non-numerical domains, we obtain different kinds of constraints.  A popular class are set constraints.
+Note: for non-numerical domains, we obtain different kinds of constraints.  A popular class are [[sav08:lecture25|set constraints]].
 ===== References =====