Mjoseh: Protegió «R4» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-03-04T17:39:30Z

Protegió «R4» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹R4: Sintaxis y semántica de la Lógica de primer orden› theory R4 imports Main begin text ‹----------------------------------…»

2020-03-04T17:39:09Z

Página creada con «<source lang = "isabelle"> chapter ‹R4: Sintaxis y semántica de la Lógica de primer orden› theory R4 imports Main begin text ‹----------------------------------…»

Página nueva

<source lang = "isabelle">

chapter ‹R4: Sintaxis y semántica de la Lógica de primer orden›

theory R4
imports Main
begin

text ‹------------------------------------------------------------------
Ejercicio 1.
(a) Formalizar el siguiente argumento (ejercicio 5 de LPO de APPLI2),
verificando la corrección de la solución:

* Todo aquel que entre en el país y no sea un VIP será cacheado por un
aduanero.
* Hay un contrabandista que entra en el país y que solo podrá ser
cacheado por contrabandistas.
* Ningún contrabandista es un VIP.
* Por lo tanto, algún aduanero es contrabandista.

(b) Escribir la formalización en Isabelle, probando la corrección del
razonamiento de forma automática o bien obteniendo un contraejemplo.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 2.
(a) Formalizar el siguiente argumento (ejercicio 15 de LPO de APPLI2),
verificando la corrección de la solución:

* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.

(b) Escribir la formalización en Isabelle, probando la corrección del
razonamiento de forma automática o bien obteniendo un contraejemplo.
Para ello, representar la constante Benito mediante el número natural
1, y la constante Álvaro mediante 2.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 3.
(a) Formalizar el siguiente argumento (ejercicio 16 de LPO de APPLI2),
verificando la corrección de la solución:

* Hay algún pez x que para cualquier pez y, si el pez x no se come al
pez y entonces existe un pez z tal que z es un tiburón o bien z
protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.

(b) Escribir la formalización en Isabelle, probando la corrección del
razonamiento de forma automática o bien obteniendo un contraejemplo.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 4.
(a) Formalizar el siguiente argumento (ejercicio 21 de LPO de APPLI2),
verificando la corrección de la solución:

* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan
a sí mismo y sólo a ellos.
* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.

(b) Escribir la formalización en Isabelle, probando la corrección del
razonamiento de forma automática o bien obteniendo un contraejemplo.
Para ello, representar la constante Carlos mediante el número natural
1.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 5.
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante.
Dar un ejemplo de una interpretación en la que F sea verdadera. Y un
ejemplo de una interpretación en la que F sea falsa.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 6.
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de
aridad 1), Q (de aridad 2) y un símbolo de función, f , de aridad 1.
Sea I = ( U, I ) la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha
estructura?
* P (x) → ∃y Q (y,x)
* ∀x Q (f(x),x)
* Q(f(x),x) → Q(x,x)
* Q(x,y) → P(x)
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 7.
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 ]
* F₂ : = ∀ x ∀ y [ f(x) = f(y) → x = y ]
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f(y) = x ]]

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos
restantes.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 8.
Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos.
Generalizarlo a un n cualquiera.
---------------------------------------------------------------------›

end

</source>

← Revisión anterior	Revisión del 17:39 4 mar 2020
(Sin diferencias)

R4 - Historial de revisiones

Mjoseh: Protegió «R4» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹R4: Sintaxis y semántica de la Lógica de primer orden› theory R4 imports Main begin text ‹----------------------------------…»