Programación Lógica (Metodo de Resolución)

[roman]

Interesante. No diré que me es totalmente desconocido pero lo que alguna vez aprendí lo tengo bastante oxidado.

Empezado por Luis Abraham

Bueno espero no haberlos enfadado con tanto rollo

Para nada. En lo personal es agradable de vez en vez ver algo totalmente ajeno a sistemas y bases de datos.

Déjame ver si he entendido algo.

Entiendo que la tautología quizá más simple es P v ~P y la contradicción quizá más sencilla es P ^ ~P

Entiendo también que (P -> Q) sea equivalente a ~P v Q, aunque me es más sencillo entenderlo primero como equivalente a ~(P ^ ~Q).

Entonces me queda claro, por ejemplo, que (P -> Q) v (Q -> P) sea una tautología. Aunque llevado a la práctica me deje un poco perplejo:

Una de las dos siguientes aseveraciones es cierta:

A. Si los pingüinos vuelan entonces los delfines caminan
B. Si los delfines caminan entonces los pingüinos vuelan

Según entiendo entonces, comprobar que una proposición es una tautología es comprobar que cualesquiera valores (F o V) que tomen sus premisas el resultado siempre será verdadero ¿cierto?

Pero vamos a ver. No me queda claro si la comprobación debe hacerse necesariamente probando cada posible valor y examinando su resultado (construir la tabla de verdad). Me explico:

Supongamos que quiero ver que (P -> Q) or (Q -> P) es una tautología. (Voy a cambiarte la notación: v=or, ^=and, ~=!)

Procedería por pasos, derivando proposiciones equivalentes:

1. (P -> Q) or (Q -> P)
2. (!P or Q) or (!Q or P) por equivalencia de implicaciones
3. !P or (Q or (!Q or P)) por asociatividad
4. !P or ((Q or !Q) or P) por asociatividad
5. !P or (true or P) por tautología
6. !P or true por tautología
7. true por tautología

Claro que no sé cómo se haría en un caso general pero quizá hay una forma canónica de reducir proposiciones a su mínima expresión.

Bueno, realmente no estoy ayudando en nada pero ¿qué quieres? Esto me gusta (aunque no lo entienda del todo) y tú empezaste .

Ahora, falta que aclares (si no hay problema) qué significa que una proposición (¿fórmula?) esté bien formada y cuáles serían las técnicas lógicas para determinarlo. Supongo que éste es el primer punto a resolver pues pienso que primero que nada hay que ver de qué manera se va a representar una fórmula ya en términos computacionales (¿Posiblemente un árbol binario?)

Oye, y ¿no sería mejor usar algo como Prolog?

// Saludos

pd: Ahora discúlpame tú por este rollo que no ayuda