Prueba de la regla de inferencia de resolución sin tabla de verdad

Question

Me encontré con la regla de inferencia de resolución que dice:

$((p\lor q)\land (\lnot p\lor r))\rightarrow(q\lor r)$

He buscado mucho en Google pero lo que me sale es la demostración mediante la tabla de verdad o usar esto para demostrar otros.

Entonces intenté algo como esto:

$LHS \equiv (p\lor q)\land (\lnot p\lor r)$

$\equiv (p\land \lnot p)\lor(p\land r)\lor (q\land \lnot p)\lor (q\land r)$

$\equiv (p\land r)\lor (q\land \lnot p)\lor (q\land r)$

Pero no puedo avanzar más.

También he intentado demostrar que toda la afirmación es cierta:

$(p\lor q)\land (\lnot p\lor r) \leftrightarrow (q\lor r)$

$\equiv \lnot((p\lor q)\land (\lnot p\lor r)) \lor (q\lor r)$

$\equiv \lnot(p\lor q)\lor \lnot(\lnot p\lor r) \lor (q\lor r)$

$\equiv (\lnot p\land \lnot q)\lor (p\land \lnot r) \lor (q\lor r)$

Pero no soy capaz de resolver esto más allá para equiparar esto a la VERDAD. ¿En qué me estoy equivocando?

Answer 1

Resolución no es una equivalencia.

La forma más fácil de derivarlo es utilizar la equivalencia tautológica entre : $A \to B$ y $\lnot A \lor B$ .

Así:

$(p∨q)∧(¬p∨r)$

es equivalente a :

$(\lnot q \to p) \land (p \to r).$

Entonces, aplicando Silogismo hipotético , obtenemos :

$\lnot q \to r$

es decir: $q \lor r$ .

Answer 2

Utilizando las equivalencias $A\lor B\equiv \neg A \to B$ y $\neg \neg A \equiv A$ Su fórmula

$((p\lor q)\land (\lnot p\lor r))\rightarrow(q\lor r)$

es equivalente a: $$((\neg p\to q)\land (p \to r)) \to (\neg q\to r)\text{,}$$ Pero $(\neg p\to q) \equiv (\neg q\to p)$ por lo que la fórmula anterior es equivalente a $$((\neg q\to p)\land (p \to r)) \to (\neg q\to r)\text{.}$$ Esto debería ser sencillo de demostrar. Detalles a petición.

Answer 3

A continuación se presenta una prueba de la regla de inferencia de resolución utilizando un comprobador de pruebas al estilo de Fitch y reglas de introducción y eliminación:

---

Editor y comprobador de pruebas de deducción natural al estilo de JavaScript/PHP de Kevin Klement http://proofs.openlogicproject.org/