Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:analyses_based_on_formulas [2009/04/08 01:19] vkuncak |
sav08:analyses_based_on_formulas [2009/04/08 01:20] vkuncak |
||
---|---|---|---|
Line 5: | Line 5: | ||
===== Fixpoint Approach ===== | ===== Fixpoint Approach ===== | ||
- | Let the domain be the set of quantifier-free formulas of first-order logic, ordered by implication | + | Let the domain be the set of quantifier-free formulas of some logic, ordered by implication |
Is this a partial order? ++|We would need to do a quotient construction to obtain it.++ | Is this a partial order? ++|We would need to do a quotient construction to obtain it.++ | ||
- | Non-existence of limits: infinite disjunction need not be a formula of our logic, e.g. | + | Non-existence of limits: infinite disjunction need not be a formula of our logic, e.g. consider formulas on linear arithmetic and take the limit |
\[ | \[ | ||
\bigvee_{i=1}^{\infty} y = i x | \bigvee_{i=1}^{\infty} y = i x | ||
\] | \] | ||
- | In general, a logic that can represent exact limits needs to express the conditions such as "there exists a sequence of statements that produces the given state". | + | 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". |
==== Approximation ==== | ==== Approximation ==== |