-- AplicacionesLP.hs
-- Aplicaciones de la Lógica proposicional.
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Librerías auxiliares --
-- ---------------------------------------------------------------------
import SintaxisSemantica
-- import TablerosSemanticos
-- import ResolucionProposicional
-- ---------------------------------------------------------------------
-- Ejercicio 1: En una isla hay dos tribus, la de los veraces (que
-- siempre dicen la verdad) y la de los mentirosos (que siempre
-- mienten). Un viajero se encuentra con tres isleños A, B y C y cada
-- uno le dice una frase A dice “B y C son veraces syss C es veraz” B
-- dice “Si A y B son veraces, entonces B y C son veraces y A es
-- mentiroso” C dice “B es mentiroso syss A o B es veraz”
--
-- Determinar a qué tribu pertenecen A, B y C.
-- Simbolización:
-- a, b y c representan que A, B y C son veraces
-- -a, -b y -c representan que A, B y C son mentirosos
-- ---------------------------------------------------------------------
-- Pedro Ros
a = Atom "a"
b = Atom "b"
c = Atom "c"
solucion1 = modelosFormula ((a<-->((b/\c)<-->c))/\(b<-->((a/\b)-->(b/\c/\(no a))))/\(c<-->((no b)<-->(a\/b))))
--*Main> solucion1
--[]
-- Todos mienten.
-- ---------------------------------------------------------------------
-- Ejercicio 2: Decidir si es posible colorear los vértices de un
-- pentágono de rojo o azul de forma que los vértices adyacentes
-- tengan colores distintos.
-- Simbolización:
-- 1, 2, 3, 4, 5 representan los vértices consecutivos del pentágono
-- ri (1 ≤ i ≤ 5) representa que el vértice i es rojo
-- ai (1 ≤ i ≤ 5) representa que el vértice i es azul
-- ---------------------------------------------------------------------
-- Pedro Ros
r1= Atom "r1"
r2= Atom "r2"
r3= Atom "r3"
r4= Atom "r4"
r5= Atom "r5"
a1= Atom "a1"
a2= Atom "a2"
a3= Atom "a3"
a4= Atom "a4"
a5= Atom "a5"
solucion2 = esSatisfacible formulacion2
where formulacion2= (((a1\/r1)/\(a2\/r2)/\(a3\/r3)/\(a4\/r4)/\(a5\/r5))/\((no(a1/\a2))/\(no(a1/\a5))/\(no(a2/\a3))/\(no(a3/\a4))/\(no(a4/\a5)))/\((no(r1/\r2))/\(no(r1/\r5))/\(no(r2/\r3))/\(no(r3/\r4))/\(no(r4/\r5))))
{-*Main> solucion2
False-}
-- ---------------------------------------------------------------------
-- Ejercicio 3: Cuatro palomas comparten tres huecos. Decidir si es
-- posible que no haya dos palomas en el mismo hueco.
-- Simbolización:
-- pihj (i ∈ {1, 2, 3, 4} y j ∈ {1, 2, 3}) representa
-- que la paloma i está en el hueco j.
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 4: Un rectángulo se divide en seis rectángulos menores como
-- se indica en la figura.
-- ------------------
-- | | B |
-- | A |----------
-- | | | |
-- |------| D | |
-- | C | | E |
-- |------|---| |
-- | F | |
-- ------------------
-- Demostrar que si cada una de los rectángulos menores tiene un lado
-- cuya medida es un número entero, entonces la medida de alguno de los
-- lados del rectángulo mayor es un número entero.
-- Simbolización:
-- base: la base del rectángulo mayor es un número entero
-- altura: la altura del rectángulo mayor es un número entero
-- base_x: la base del rectángulo X es un número entero
-- altura_x: la altura del rectángulo X es un número entero
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 5: Calcular las formas de colocar 4 reinas en un tablero
-- de 4x4 de forma que no haya más de una reina en cada fila,
-- columna o diagonal.
-- Simbolización:
-- cij (1 ≤ i, j ≤ 4) indica que hay una reina en la fila i columna j.
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Ejercicio 6: Probar el caso más simple del teorema de Ramsey: entre
-- seis personas siempre hay (al menos) tres tales que cada una conoce
-- a las otras dos o cada una no conoce a ninguna de las otras dos.
-- Simbolización:
-- 1,2,3,4,5,6 representan a las personas
-- pij (1 ≤ i < j ≤ 6) indica que las personas i y j se conocen.
-- ---------------------------------------------------------------------
