Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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) =====
 
sav08/homework05.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice