• English only

# Differences

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

 sav08:quantifier_elimination_definition [2009/04/22 14:20]vkuncak sav08:quantifier_elimination_definition [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2011/04/05 16:02 vkuncak 2009/04/22 14:20 vkuncak 2009/04/22 10:07 vkuncak 2009/04/22 10:07 vkuncak 2009/04/21 23:42 vkuncak 2009/04/21 19:23 vkuncak 2009/04/21 19:10 vkuncak 2009/04/21 19:09 vkuncak 2009/04/21 18:57 vkuncak 2008/04/10 01:36 vkuncak 2008/04/10 01:35 vkuncak 2008/04/10 01:35 vkuncak 2008/04/09 21:35 vkuncak 2008/04/09 21:29 vkuncak 2008/04/09 21:29 vkuncak created Next revision Previous revision 2011/04/05 16:02 vkuncak 2009/04/22 14:20 vkuncak 2009/04/22 10:07 vkuncak 2009/04/22 10:07 vkuncak 2009/04/21 23:42 vkuncak 2009/04/21 19:23 vkuncak 2009/04/21 19:10 vkuncak 2009/04/21 19:09 vkuncak 2009/04/21 18:57 vkuncak 2008/04/10 01:36 vkuncak 2008/04/10 01:35 vkuncak 2008/04/10 01:35 vkuncak 2008/04/09 21:35 vkuncak 2008/04/09 21:29 vkuncak 2008/04/09 21:29 vkuncak created Line 2: Line 2: In this section, we will consider some language ${\cal L}$ and some set $T$ of formulas such that $Conseq(T)=T$ (see [[sav08:​First-Order Logic Semantics]]). ​ In this section, we will consider some language ${\cal L}$ and some set $T$ of formulas such that $Conseq(T)=T$ (see [[sav08:​First-Order Logic Semantics]]). ​ + + //Informal summary: the meaning of relations and functions such as <,+, can be defined by starting from first-order logic, and then introducing a set of axioms in first-order logic that they satisfy, and taking also their consequences. The set of axioms and consequences that define the operations and relations of interest is the theory. Formally, the theory is simply any set of fully quantified formulas (often the theory is understood to also include all of its consequences).//​ As a special case, we can have As a special case, we can have - $+ \begin{equation*} T = \{ F \mid \forall I \in {\cal I}. e_F(F)(I) \} T = \{ F \mid \forall I \in {\cal I}. e_F(F)(I) \} -$ + \end{equation*} where ${\cal I}$ is a set of interpretations of interest. where ${\cal I}$ is a set of interpretations of interest. Then $\models F$ reduces to $\forall I \in {\cal I}. e_F(F)(I)$. Then $\models F$ reduces to $\forall I \in {\cal I}. e_F(F)(I)$. Line 34: Line 36: Example: in language ${\cal L} = \{0,1,+\}$ where $0,1$ are constants and $+$ is a binary operation, an example of a ground formula is Example: in language ${\cal L} = \{0,1,+\}$ where $0,1$ are constants and $+$ is a binary operation, an example of a ground formula is - $+ \begin{equation*} \lnot (0 = 1) \rightarrow \lnot (0 + 1 = 1 + 1) \lnot (0 = 1) \rightarrow \lnot (0 + 1 = 1 + 1) -$ + \end{equation*} **Lemma:** Suppose that **Lemma:** Suppose that

sav08/quantifier_elimination_definition.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice 