Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:homework05 [2008/03/25 14:17] piskac |
sav08:homework05 [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Homework 05 - due 2 April 2008 (after break) ====== | ====== Homework 05 - due 2 April 2008 (after break) ====== | ||
+ | |||
+ | |||
Line 21: | Line 23: | ||
Test examples shown in the class: | Test examples shown in the class: | ||
- | [[dpll:test.cnf]] | + | [[dpll:test.cnf]] [[dpll:test2.cnf]] [[dpll:test3.cnf]] |
- | [[http://icwww.epfl.ch/~piskac/test.cnf|test.cnf]]. | ||
- | [[http://icwww.epfl.ch/~piskac/test2.cnf|test2.cnf]]. | ||
- | [[http://icwww.epfl.ch/~piskac/test3.cnf|test3.cnf]]. | ||
===== Problem 2 ===== | ===== Problem 2 ===== | ||
Line 36: | Line 35: | ||
**Part c)** Prove (using appropriate proof technique) that your definition of fsfsubst has the property | **Part c)** Prove (using appropriate proof technique) that your definition of fsfsubst has the property | ||
- | \[ | + | \begin{equation*} |
e_F(fsfsubst(\{x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\})(F))(I) = e_F(F)(I[x_1 \mapsto e_T(t_1)(I),\ldots, x_n \mapsto e_T(t_n)(I)]) | e_F(fsfsubst(\{x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\})(F))(I) = e_F(F)(I[x_1 \mapsto e_T(t_1)(I),\ldots, x_n \mapsto e_T(t_n)(I)]) | ||
- | \] | + | \end{equation*} |
You can assume that formulas are built using only these symbols: | You can assume that formulas are built using only these symbols: | ||
* one constant $a$ | * one constant $a$ | ||
Line 49: | Line 48: | ||
Consider the definition of [[First-Order Logic Semantics#Consequence set]] defined in [[First-Order Logic Semantics]]. | Consider the definition of [[First-Order Logic Semantics#Consequence set]] defined in [[First-Order Logic Semantics]]. | ||
Prove that it satisfies these properties where $T_1$, $T_2$ denote sets of formulas. | Prove that it satisfies these properties where $T_1$, $T_2$ denote sets of formulas. | ||
- | \[ | + | \begin{equation*} |
\begin{array}{rcl} | \begin{array}{rcl} | ||
T &\subseteq & Conseq(T) \\ | T &\subseteq & Conseq(T) \\ | ||
Line 56: | Line 55: | ||
T_1 \subseteq Conseq(T_2) \land T_2 \subseteq Conseq(T_1) & \rightarrow & Conseq(T_1) = Conseq(T_2) | T_1 \subseteq Conseq(T_2) \land T_2 \subseteq Conseq(T_1) & \rightarrow & Conseq(T_1) = Conseq(T_2) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
===== Problem 4 (Optional) ===== | ===== Problem 4 (Optional) ===== |