Lógica informática (2014-15) - Contribuciones del usuario [es]

Relación 10

2014-12-03T18:12:42Z

Mjoseh: Página creada con '=== Relación 10: Temas 1 a 8 === ---- '''Ejercicio 1.''' Formalizar el siguiente argumento: <blockquote> Quien desprecia a todos los fanáticos desprecia también a todos los ...'

=== Relación 10: Temas 1 a 8 ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento:
<blockquote>
Quien desprecia a todos los fanáticos desprecia también a todos los políticos. Alguien no desprecia a un determinado político. Por consiguiente, hay un fanático al que no todo el mundo desprecia.
</blockquote>

Nota: Comprobar la formalización con [http://bit.ly/1pkvwsf APLI2].
----

'''Solución:'''

----
'''Ejercicio 2.''' En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
: F = ∀ x [ f ( x ) = a ] ,
: G = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
: H = ∀ x [ x = a → ∃ y [ f ( y ) = x ]] .

Decidir si alguna de estas fórmulas es consecuencia lógica de las dos restantes.

----

'''Solución:'''

----
'''Ejercicio 3.''' Probar por deducción natural
: ∀x ∀ y (P(y) → Q(x)) ⊢ ∃y P(y) → ∀x Q(x)

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, mediante tableros semáticos, si la fórmula
: (p ∧ q ↔ p ∨ q) → (p → q)

es una tautología.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir, por resolución, si la fórmula p ↔ p ∨ r es consecuencia lógica de la fórmula q → p ∧ r.
----

'''Solución:'''

R10

2014-12-03T18:12:30Z

Mjoseh: Protegió «R10» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

R10

2014-12-03T18:12:16Z

Mjoseh:

R10

2014-12-03T18:11:46Z

Mjoseh:

=== Relación 10: Temas 1 a 8 ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento:
<blockquote>
Quien desprecia a todos los fanáticos desprecia también a todos los políticos. Alguine no desprecia a un determinado político. Por consiguiente, hay un fanático al que no todo el mundo desprecia.
</blockquote>

Nota: Comprobar la formalización con [http://bit.ly/1pkvwsf APLI2].
----

'''Solución:'''

----
'''Ejercicio 2.''' En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
: F = ∀ x [ f ( x ) = a ] ,
: G = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
: H = ∀ x [ x = a → ∃ y [ f ( y ) = x ]] .

Decidir si alguna de estas fórmulas es consecuencia lógica de las dos restantes.

----

'''Solución:'''

----
'''Ejercicio 3.''' Probar por deducción natural
: ∀x ∀ y (P(y) → Q(x)) ⊢ ∃y P(y) → ∀x Q(x)

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, mediante tableros semáticos, si la fórmula
: (p ∧ q ↔ p ∨ q) → (p → q)

es una tautología.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir, por resolución, si la fórmula p ↔ p ∨ r es consecuencia lógica de la fórmula q → p ∧ r.
----

'''Solución:'''

R10

2014-12-03T18:10:44Z

=== Relación 10: Temas 1 a 8 ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento:
<blockquote>
Quien desprecia a todos los fanáticos desprecia también a todos los políticos. Alguine no desprecia a un determinado político. Por consiguiente, hay un fanático al que no todo el mundo desprecia.
</blockquote>

Nota: Comprobar la formalización con [http://bit.ly/1pkvwsf APLI2].
----

'''Solución:'''

----
'''Ejercicio 2.''' En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
: F_1 = ∀ x [ f ( x ) = a ] ,
: F_2 = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
: F_3 = ∀ x [ x = a → ∃ y [ f ( y ) = x ]] .

Decidir si alguna de estas fórmulas es consecuencia lógica de las dos restantes.

----

'''Solución:'''

----
'''Ejercicio 3.''' Probar por deducción natural
: ∀x ∀ y (P(y) → Q(x)) ⊢ ∃y P(y) → ∀x Q(x)

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, mediante tableros semáticos, si la fórmula
: (p ∧ q ⇔ p ∨ q) → (p → q)

es una tautología.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir, por resolución, si la fórmula p ↔ p ∨ r es consecuencia lógica de la fórmula q → p ∧ r.
----

'''Solución:'''

Lógica informática (2014-15)

2014-12-03T18:10:25Z

Mjoseh:

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas. Para escribir las fórmulas lógicas se puede usar cualquier editor de símbolos matemáticos como [http://math.typeit.org Type mathematical symbols] (los símbolos lógicos son ¬, ∧, ∨, →, ↔ y ⊧).

* '''Relación 1''': Tema 1 (a). ([[R1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Tema 1 (b). ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Temas 1 y 2. ([[R3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Temas 1 y 2. ([[R4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Temas 1 a 4. ([[R5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Temas 1 a 5. ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Temas 1 a 6. ([[R7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]). [[http://www.cs.us.es/~jalonso/cursos/li/ejercicios/R7_sol.html Solución]].
* '''Relación 8''': Temas 1 a 7. ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]). [[http://www.cs.us.es/~jalonso/cursos/li/ejercicios/R8_sol.html Solución]].
* '''Relación 9''': Temas 1 a 7. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Temas 1 a 8. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).

Relación 7

2014-11-09T18:13:50Z

Mjoseh:

=== Relación 7: Temas 1 a 6 ===

----
'''Ejercicio 1.''' Sean S y T conjuntos de fórmulas. Demostrar o refutar las siguientes sentencias:
* Si S es consistente y T es inconsistente, entonces S ∪ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∪ T es inconsistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es inconsistente.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar por deducción natural, tableros semánticos y resolución
: ¬(p ∧ ¬q) ⊧ p → q
----

'''Solución:'''

----
'''Ejercicio 3.''' Un pirata se encuentra con cuatro cofres y una inscripción
en cada uno de ellos. En el primer cofre dice "El tesoro no está aquí". En el
segundo, dice "El tesoro está en el cofre 3". En el tercero dice "El cofre 1
dice la verdad". Y, en el cuarto dice "El cofre 2 miente". Ayuda al pirata a
encontrar el tesoro, sabiendo que de los cuatro letreros, al menos tres mienten.

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, utilizando formas normales, si la fórmula
: (p → ¬(q → ¬r)) ∧ (r → ¬q)
es insatisfactible o una tautología.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir, usando el algoritmo DPLL y resolución, si el
conjunto de cláusulas
:{{p,r,¬s}, {¬q,s}, {¬p,¬s,¬r}, {¬p,s,q},{s,q,p}, {¬q,¬r}, {¬s,¬r,p}}
es consistente. En caso de que lo sea, proporcionar un modelo del mismo.
----

'''Solución:'''

R7

2014-11-05T18:01:06Z

Mjoseh: Protegió «R7» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

=== Relación 7: Temas 1 a 6 ===

----
'''Ejercicio 1.''' Sean S y T conjuntos de fórmulas. Demostrar o refutar las siguientes sentencias:
* Si S es consistente y T es inconsistente, entonces S ∪ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∪ T es inconsistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es inconsistente.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar por deducción natural, tableros semánticos y resolución
: ¬(p ∧ ¬q) ⊧ p → q
----

'''Solución:'''

----
'''Ejercicio 3.''' Un pirata se encuentra con cuatro cofres y una inscripción
en cada uno de ellos. En el primer cofre dice "El tesoro no está aquí". En el
segundo, dice "El tesoro está en el cofre 3". En el tercero dice "El cofre 1
dice la verdad". Y, en el cuarto dice "El cofre 2 miente". Ayuda al pirata a
encontrar el tesoro, sabiendo que de los tres letreros, al menos tres mienten.

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, utilizando formas normales, si la fórmula
: (p → ¬(q → ¬r)) ∧ (r → ¬q)
es insatisfactible o una tautología.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir, usando el algoritmo DPLL y resolución, si el
conjunto de cláusulas
:{{p,r,¬s}, {¬q,s}, {¬p,¬s,¬r}, {¬p,s,q},{s,q,p}, {¬q,¬r}, {¬s,¬r,p}}
es consistente. En caso de que lo sea, proporcionar un modelo del mismo.
----

'''Solución:'''

Relación 7

2014-11-05T18:00:50Z

Mjoseh: Página creada con '=== Relación 7: Temas 1 a 6 === ---- '''Ejercicio 1.''' Sean S y T conjuntos de fórmulas. Demostrar o refutar las siguientes sentencias: * Si S es consistente y T es inconsis...'

=== Relación 7: Temas 1 a 6 ===

----
'''Ejercicio 1.''' Sean S y T conjuntos de fórmulas. Demostrar o refutar las siguientes sentencias:
* Si S es consistente y T es inconsistente, entonces S ∪ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∪ T es inconsistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es inconsistente.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar por deducción natural, tableros semánticos y resolución
: ¬(p ∧ ¬q) ⊧ p → q
----

'''Solución:'''

----
'''Ejercicio 3.''' Un pirata se encuentra con cuatro cofres y una inscripción
en cada uno de ellos. En el primer cofre dice "El tesoro no está aquí". En el
segundo, dice "El tesoro está en el cofre 3". En el tercero dice "El cofre 1
dice la verdad". Y, en el cuarto dice "El cofre 2 miente". Ayuda al pirata a
encontrar el tesoro, sabiendo que de los tres letreros, al menos tres mienten.

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, utilizando formas normales, si la fórmula
: (p → ¬(q → ¬r)) ∧ (r → ¬q)
es insatisfactible o una tautología.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir, usando el algoritmo DPLL y resolución, si el
conjunto de cláusulas
:{{p,r,¬s}, {¬q,s}, {¬p,¬s,¬r}, {¬p,s,q},{s,q,p}, {¬q,¬r}, {¬s,¬r,p}}
es consistente. En caso de que lo sea, proporcionar un modelo del mismo.
----

'''Solución:'''

R7

2014-11-05T18:00:42Z

=== Relación 7: Temas 1 a 6 ===

----
'''Ejercicio 1.''' Sean S y T conjuntos de fórmulas. Demostrar o refutar las siguientes sentencias:
* Si S es consistente y T es inconsistente, entonces S ∪ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∪ T es inconsistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es consistente.
* Si S es consistente y T es inconsistente, entonces S ∩ T es inconsistente.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar por deducción natural, tableros semánticos y resolución
: ¬(p ∧ ¬q) ⊧ p → q
----

'''Solución:'''

----
'''Ejercicio 3.''' Un pirata se encuentra con cuatro cofres y una inscripción
en cada uno de ellos. En el primer cofre dice "El tesoro no está aquí". En el
segundo, dice "El tesoro está en el cofre 3". En el tercero dice "El cofre 1
dice la verdad". Y, en el cuarto dice "El cofre 2 miente". Ayuda al pirata a
encontrar el tesoro, sabiendo que de los tres letreros, al menos tres mienten.

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, utilizando formas normales, si la fórmula
: (p → ¬(q → ¬r)) ∧ (r → ¬q)
es insatisfactible o una tautología.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir, usando el algoritmo DPLL y resolución, si el
conjunto de cláusulas
:{{p,r,¬s}, {¬q,s}, {¬p,¬s,¬r}, {¬p,s,q},{s,q,p}, {¬q,¬r}, {¬s,¬r,p}}
es consistente. En caso de que lo sea, proporcionar un modelo del mismo.
----

'''Solución:'''

Lógica informática (2014-15)

2014-11-05T18:00:21Z

Mjoseh:

R6

2014-10-31T11:40:20Z

Mjoseh:

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos
: {p ↔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, mediante tableros semánticos, formas normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

----
'''Ejercicio 5.''' Formalizar el siguiente razonamiento y probar que es
correcto, mediante deducción natural.
<blockquote>
Si el general era leal, hubiera obedecido las órdenes, y si era inteligente las
hubiera comprendido. O el general desobedeció las órdenes o no las
comprendió. Por lo tanto, el general era desleal o no era inteligente.
</blockquote>

----

'''Solución:'''

Relación 6

2014-10-31T11:38:48Z

Mjoseh:

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

I⊨S_1 ↦ I⊨{S_1,1 , S_1,1 , … , S_(1,n)} ↦ I⊨S_1,1∧ S_1,1∧…∧S_(1,n)

En el operador ∧ con que uno de sus operandos sea falso todo es falso. Si existe un una interpretación para S_1, ese modelo también lo será para cualquier subconjunto, en este caso, S_2

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos
: {p ↔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir, mediante tableros semánticos, formas normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

----
'''Ejercicio 5.''' Formalizar el siguiente razonamiento y probar, mediante deducción natural, que es
correcto.
<blockquote>
Si el general era leal, hubiera obedecido las órdenes, y si era inteligente las
hubiera comprendido. O el general desobedeció las órdenes o no las
comprendió. Por lo tanto, el general era desleal o no era inteligente.
</blockquote>

----

'''Solución:'''

Relación 6

2014-10-31T11:36:51Z

Mjoseh:

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

I⊨S_1 ↦ I⊨{S_1,1 , S_1,1 , … , S_(1,n)} ↦ I⊨S_1,1∧ S_1,1∧…∧S_(1,n)

En el operador ∧ con que uno de sus operandos sea falso todo es falso. Si existe un una interpretación para S_1, ese modelo también lo será para cualquier subconjunto, en este caso, S_2

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos
: {p ↔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar que mediante tableros semánticos, formas normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

----
'''Ejercicio 5.''' Formalizar el siguiente razonamiento y probar que es
correcto, mediante deducción natural.
<blockquote>
Si el general era leal, hubiera obedecido las órdenes, y si era inteligente las
hubiera comprendido. O el general desobedeció las órdenes o no las
comprendió. Por lo tanto, el general era desleal o no era inteligente.
</blockquote>

----

'''Solución:'''

R6

2014-10-29T11:36:06Z

Mjoseh: Protegió «R6» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos
: {p ↔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar que mediante deducción natural, tableros semánticos, formas normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

Relación 6

2014-10-29T11:34:41Z

Mjoseh: Página creada con '=== Relación 6: Temas 1 a 5 === ---- '''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un modelo de una hoja abierta de T y S2 es un subconjunto de S1, en...'

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos
: {p ↔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar que mediante deducción natural, tableros semánticos, formas normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

R6

2014-10-29T11:34:21Z

Mjoseh:

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos
: {p ↔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar que mediante deducción natural, tableros semánticos, formas normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

R6

2014-10-29T11:28:01Z

Mjoseh:

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos
: {p ⇔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar que mediante deducción natural, tableros semánticos, formas normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

R6

2014-10-29T11:27:16Z

Mjoseh:

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos:
: {p ⇔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2, C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar que mediante deducción natural, tableros semánticos, formas
normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

R6

2014-10-29T11:26:22Z

=== Relación 6: Temas 1 a 5 ===

----
'''Ejercicio 1.''' Demostrar o refutar: Si T es un tablero de S1, I es un
modelo de una hoja abierta de T y S2 es un subconjunto de S1, entonces, I es
modelo de S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Decidir la consistencia del siguiente conjunto de fórmulas,
mediante resolución proposicional y tableros semánticos:
: {p ⇔ ¬q, q → p, r → q, q → r ∧ p, (¬q → r) ∨ p }
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes sentencias:
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2,
D ⊂ C1 y D ≠ C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2 y
D = C1.
* Existen cláusulas C1, C2 y D tales que D es una resolvente de C1 y C2,
C1 ⊂ D y C2 no es una tautología.
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar que mediante deducción natural, tableros semánticos, formas
normales y resolución
:{C → A, G → D, ¬(B ∧ C ∧ G → E)} ⊧ A ∧ B ∧ C,

----

'''Solución:'''

Lógica informática (2014-15)

2014-10-29T11:18:32Z

Mjoseh:

R3

2014-10-08T07:43:41Z

Mjoseh:

=== Relación 3: Temas 1 y 2 ===

----
'''Ejercicio 1.''' Formalizar, y decidir la corrección, del siguiente argumento
<blockquote>
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo haría. Si Dios fuera incapaz de evitar el mal, no sería omnipotente; si no quisiera evitar el mal sería malévolo. Dios no evita el mal. Si Dios existe, es omnipotente y no es malévolo. Luego, Dios no existe.
</blockquote>
Usando los símbolos C: Dios es capaz de evitar el mal, Q: Dios quiere evitar el mal, O: Dios es omnipotente, M: Dios es malévolo, P: Dios evita el mal, E: Dios existe.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar las siguiente proposición: Para todo conjunto de fórmula S y para toda fórmula F se verifica que si F no es consecuencia de S, entonces ¬F es consecuencia de S.
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar mediante deducción natural:
: (p → q) → r ⊧ p → (q → r)
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar mediante deducción natural:
: (p → q) ∧ (p → r) ⊧ p → q ∧ r
----

'''Solución:'''

----
'''Ejercicio 5.''' Demostrar mediante deducción natural:
: (p → r) ∧ (q → r) ⊧ p ∨ q → r
----

'''Solución:'''

----
'''Ejercicio 6.''' Demostrar mediante deducción natural:
: {p → r, r → ¬ q} ⊧ ¬(p ∧ q)
----

'''Solución:'''