Logika dla informatyków/Ćwiczenia 2: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Linia 1: Linia 1:
Ćwiczenie 1<br>
+
{{Cwiczenie|1||
  
 
Niech <math>\mathfrak =<\mathbb N, p^\mathfrak A, q^\mathfrak A ></math>, gdzie:  
 
Niech <math>\mathfrak =<\mathbb N, p^\mathfrak A, q^\mathfrak A ></math>, gdzie:  
Linia 13: Linia 13:
  
 
są spełnione przy wartościowaniu <math>v(y) = 7</math>, <math>v(z) = 1</math> w strukturze <math>\mathfrak A</math>.  
 
są spełnione przy wartościowaniu <math>v(y) = 7</math>, <math>v(z) = 1</math> w strukturze <math>\mathfrak A</math>.  
 +
}}
  
 
+
{{Cwiczenie|2||
Ćwiczenie 2<br>
 
 
Niech <math>\mathfrak A = \<\mathbb Z, f^\mathfrak A, r^\mathfrak A ></math> i <math>\mathfrak B = \< \mathbb Z, f^\mathfrak b, r^\mathfrak b ></math>, gdzie   
 
Niech <math>\mathfrak A = \<\mathbb Z, f^\mathfrak A, r^\mathfrak A ></math> i <math>\mathfrak B = \< \mathbb Z, f^\mathfrak b, r^\mathfrak b ></math>, gdzie   
 
<center><math>f^\mathfrak A (m,n) = min(m,n)</math>, dla <math>m,n\in\mathbb ZZ</math>, a <math>r^\mathfrak A</math> jest   
 
<center><math>f^\mathfrak A (m,n) = min(m,n)</math>, dla <math>m,n\in\mathbb ZZ</math>, a <math>r^\mathfrak A</math> jest   
Linia 26: Linia 26:
  
 
są spełnione przy wartościowaniu  <math>v(z) =5</math>, <math>v(y)=7</math> w strukturach <math>\mathfrak A</math> i <math>\mathfrak B</math>.  
 
są spełnione przy wartościowaniu  <math>v(z) =5</math>, <math>v(y)=7</math> w strukturach <math>\mathfrak A</math> i <math>\mathfrak B</math>.  
 +
}}
  
 
+
{{Cwiczenie|3||
Ćwiczenie 3<br>
 
 
Czy formuła <math>\forall x(\neg r(x,y)\to\exists z(r(f(x,z),g(y))))</math> jest spełniona przy wartościowaniu <math>v(x) =3</math>, <math>w(x) = 6</math> i <math>u(x) = 14</math>  
 
Czy formuła <math>\forall x(\neg r(x,y)\to\exists z(r(f(x,z),g(y))))</math> jest spełniona przy wartościowaniu <math>v(x) =3</math>, <math>w(x) = 6</math> i <math>u(x) = 14</math>  
 
#w strukturze <math>\mathfrak A = <\mathbb N, r^\mathfrak A ></math>, gdzie <math>r^\mathfrak A</math> jest  relacją podzielności?  
 
#w strukturze <math>\mathfrak A = <\mathbb N, r^\mathfrak A ></math>, gdzie <math>r^\mathfrak A</math> jest  relacją podzielności?  
 
#w strukturze <math>\mathfrak B = <\mathbb N, r^\mathfrak B ></math>, gdzie <math>r^\mathfrak B</math> jest relacją przystawania modulo 7?  
 
#w strukturze <math>\mathfrak B = <\mathbb N, r^\mathfrak B ></math>, gdzie <math>r^\mathfrak B</math> jest relacją przystawania modulo 7?  
 +
}}
  
 
+
{{Cwiczenie|4||
Ćwiczenie 4<br>
 
 
W jakich strukturach prawdziwa jest formuła <math>\exists y (y\neq x)</math>?  A&nbsp;formuła <math>\exists y (y\neq y)</math>  
 
W jakich strukturach prawdziwa jest formuła <math>\exists y (y\neq x)</math>?  A&nbsp;formuła <math>\exists y (y\neq y)</math>  
 
otrzymana przez "naiwne" podstawienie <math>y</math> na <math>x</math>?   
 
otrzymana przez "naiwne" podstawienie <math>y</math> na <math>x</math>?   
 +
}}
  
 
+
{{Cwiczenie|5||
Ćwiczenie 5<br>
 
 
Podaj przykład modelu i wartościowania, przy którym formuła   
 
Podaj przykład modelu i wartościowania, przy którym formuła   
 
<center><math>p(x,f(x)) \to \forall x\exists y p(f(y),x)</math> </center>
 
<center><math>p(x,f(x)) \to \forall x\exists y p(f(y),x)</math> </center>
  
 
jest: a) spełniona  b) nie spełniona.  
 
jest: a) spełniona  b) nie spełniona.  
 +
}}
  
 
+
{{Cwiczenie|6||
Ćwiczenie 6<br>
 
 
Zbadać, czy następujące formuły są tautologiami  i czy są spełnialne:
 
Zbadać, czy następujące formuły są tautologiami  i czy są spełnialne:
  
Linia 53: Linia 53:
 
#<math>\exists x(\forall y q(y)\to p(x))\to \exists x\forall y(q(y)\to p(x))</math>;  
 
#<math>\exists x(\forall y q(y)\to p(x))\to \exists x\forall y(q(y)\to p(x))</math>;  
 
#<math>\exists x(\forall y q(y)\to p(x)) \to\exists x(q(x)\to p(x))</math>.  
 
#<math>\exists x(\forall y q(y)\to p(x)) \to\exists x(q(x)\to p(x))</math>.  
 +
}}
  
 
+
{{Cwiczenie|7||
Ćwiczenie 7<br>
 
 
Niech <math>f</math> będzie jednoargumentowym symbolem funkcyjnym, który nie występuje w&nbsp;formule&nbsp;<math>\var\varphi</math>.  
 
Niech <math>f</math> będzie jednoargumentowym symbolem funkcyjnym, który nie występuje w&nbsp;formule&nbsp;<math>\var\varphi</math>.  
 
Pokazać, że formuła <math>\forall x\exists y \var\varphi</math> jest spełnialna  
 
Pokazać, że formuła <math>\forall x\exists y \var\varphi</math> jest spełnialna  
 
wtedy i tylko wtedy gdy formuła <math>\forall x \var\varphi[f(x)/y]</math> jest   
 
wtedy i tylko wtedy gdy formuła <math>\forall x \var\varphi[f(x)/y]</math> jest   
 
spełnialna.   
 
spełnialna.   
 +
}}
  
 
+
{{Cwiczenie|8||
Ćwiczenie 8<br>
 
 
Udowodnić, że zdanie  
 
Udowodnić, że zdanie  
 
<cemter><math>\forall x\exists y p(x,y)\wedge \forall x\neg p(x,x) \wedge \forall x\forall y\forall z(p(x,y)\wedge p(y,z)\to p(x,z))</math>.  
 
<cemter><math>\forall x\exists y p(x,y)\wedge \forall x\neg p(x,x) \wedge \forall x\forall y\forall z(p(x,y)\wedge p(y,z)\to p(x,z))</math>.  
 
ma tylko modele nieskończone.   
 
ma tylko modele nieskończone.   
 +
}}
  
 
+
{{Cwiczenie|9||
Ćwiczenie 9<br>
 
 
Dla każdego <math>n</math> napisać takie zdanie <math>\var\varphi_n</math>, że   
 
Dla każdego <math>n</math> napisać takie zdanie <math>\var\varphi_n</math>, że   
 
<math>\mathfrak A\models\var\varphi_n</math> zachodzi \wtw, gdy <math>\mathfrak A</math> ma dokładnie   
 
<math>\mathfrak A\models\var\varphi_n</math> zachodzi \wtw, gdy <math>\mathfrak A</math> ma dokładnie   
 
<math>n</math>elementów.  
 
<math>n</math>elementów.  
 +
}}
  
 
+
{{Cwiczenie|10||
Ćwiczenie 10<br>
 
 
Czy jeśli <math>\mathfrak A \models \exists x \var\varphi</math>, to także  
 
Czy jeśli <math>\mathfrak A \models \exists x \var\varphi</math>, to także  
 
<math>\mathfrak A \models \var\varphi[t/x]</math>, dla pewnego termu <math>t</math>?
 
<math>\mathfrak A \models \var\varphi[t/x]</math>, dla pewnego termu <math>t</math>?
 +
}}

Wersja z 09:22, 29 wrz 2006

Ćwiczenie 1

Niech , gdzie:

wtedy i tylko wtedy, gdy ;
wtedy i tylko wtedy, gdy
.

Zbadać czy formuły

    1. ;
    2. ;
    3. ;

są spełnione przy wartościowaniu , w strukturze .

Ćwiczenie 2

Niech Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathfrak A = \<\mathbb Z, f^\mathfrak A, r^\mathfrak A >} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathfrak B = \< \mathbb Z, f^\mathfrak b, r^\mathfrak b >} , gdzie

, dla , a jest

relacją ;
, dla , a jest relacją .

Zbadać czy formuły

  1. ;
  2. ,

są spełnione przy wartościowaniu , w strukturach i .

Ćwiczenie 3

Czy formuła jest spełniona przy wartościowaniu , i

  1. w strukturze , gdzie jest relacją podzielności?
  2. w strukturze , gdzie jest relacją przystawania modulo 7?

Ćwiczenie 4

W jakich strukturach prawdziwa jest formuła ? A formuła otrzymana przez "naiwne" podstawienie na ?

Ćwiczenie 5

Podaj przykład modelu i wartościowania, przy którym formuła

jest: a) spełniona b) nie spełniona.

Ćwiczenie 6

Zbadać, czy następujące formuły są tautologiami i czy są spełnialne:

  1. ;
  2. ;
  3. ;
  4. .

Ćwiczenie 7

Niech będzie jednoargumentowym symbolem funkcyjnym, który nie występuje w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Pokazać, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\exists y \var\varphi} jest spełnialna wtedy i tylko wtedy gdy formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x \var\varphi[f(x)/y]} jest spełnialna.

Ćwiczenie 8

Udowodnić, że zdanie <cemter>. ma tylko modele nieskończone.

Ćwiczenie 9

Dla każdego napisać takie zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n} , że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\models\var\varphi_n} zachodzi \wtw, gdy ma dokładnie elementów.

Ćwiczenie 10

Czy jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A \models \exists x \var\varphi} , to także Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A \models \var\varphi[t/x]} , dla pewnego termu ?