Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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