• English only

# Differences

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

sav08:homework05 [2008/03/25 14:22]
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 24: Line 25:
[[dpll:​test.cnf]] [[dpll:​test2.cnf]] [[dpll:​test3.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 37: 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 50: 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 57: 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) =====