Skip to content
Snippets Groups Projects
Commit 6f5a7ab2 authored by Etienne Levecque's avatar Etienne Levecque
Browse files

Merge branch 'master' into 'master'

parents 8d503da2 42454b2f
No related branches found
No related tags found
No related merge requests found
# Exercise 4.4
(a) Let $`\varphi`$ and $`\psi`$ be equivalent conjunctive calculus formulas, and suppose that $`\Psi^{\prime}`$ is the result of replacing an occurrence of $`\varphi`$ by $`\psi`$ in conjunctive calculus formula $`\Psi`$. Prove that $`\Psi`$ and $`\Psi^{\prime}`$ are equivalent.
(b) Prove that the application of the rewrite rules rename and merge-exists to a conjunctive calculus formula yields an equivalent formula.
(c) Prove that these rules can be used to transform any conjunctive calculus formula into
an equivalent formula in normal form.
* * *
### Rony
a)
Let's recall that : Conjunctive calculus formulas ϕ and ψ over **R** are equivalent if **they have the same
free variables** and, for each **I** over **R** and valuation $`ν`$ over free(ϕ) = free(ψ),
**I |= ϕ[ν] iff I |= ψ[ν].**
Let's say that : $`\Psi = \Phi \ \varphi \ \Phi^{\prime}`$ . In that case $`\Psi^{\prime} = \Phi \ \psi \ \Phi^{\prime}`$.
$`\blacksquare`$ Clearly, $`free(\Psi)=free(\varphi) \ \text{and} \ free(\Psi^{\prime})=free(\psi)`$
By hypothesis, $`\varphi`$ and $`\psi`$ are equivalent and so :
$`free(\Psi)=free(\varphi)=free(\psi)=free(\Psi^{\prime})`$
$`\blacksquare`$ Let's **I** an instance over **R** and $`v`$ a valuation over $`free(\Psi)=free(\Psi^{\prime})`$.
Clearly I|=$`\Psi[v]`$
iff (I|=$`\Phi[v]`$ and I|=$`\varphi[v]`$ and I|=$`\Phi^{\prime}[v]`$)
iff (I|=$`\Phi[v]`$ and I|=$`\psi[v]`$ and I|=$`\Phi^{\prime}[v]`$) because $`\varphi`$ and $`\psi`$ are equivalent.
iff I|=$`\Psi^{\prime}[v]`$
### So Finally, $`\Psi`$ and $`\Psi^{\prime}`$ are equivalent.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment