Pruebas e inferencias en la demostración del teorema proposicional

Este artículo analiza cómo usar las reglas de inferencia para crear pruebas: una serie de conclusiones que conducen al resultado deseado. La regla más conocida se conoce como Modus Ponens (modo afirmativo en latín) y se expresa como

$\frac{\alpha \Rightarrow \beta, \quad \alpha}{\beta}$

Inferencias en la demostración del teorema proposicional

La notación significa que la oración puede deducirse siempre que se suministren oraciones de este tipo. Si $\text { ( WumpusAhead } \wedge \text { WumpusAlive) } \Rightarrow \text { Shoot }$ y $\text { (WumpusAhead } \wedge \text { WumpusAlive) }$ se proporcionan ambos, se puede deducir Shoot.

Y-Eliminación es otra regla de inferencia útil, que establece que cualquiera de los conjuntos se puede inferir de la conjunción:

$\frac{\alpha \wedge \beta}{\alpha}$

WumpusAlive se puede deducir de $\text { (WumpusAhead } \wedge \text { WumpusAlive) }$ , por ejemplo. Uno puede demostrar fácilmente que Modus Ponens y And-Elimination son sólidos de una vez por todas al evaluar los valores de verdad potenciales de $\alpha$ y $\beta$ . Estos principios pueden luego aplicarse a cada situación en la que se apliquen, dando como resultado buenas conclusiones sin la necesidad de enumerar modelos.

$\begin{aligned} (\alpha \wedge \beta) & \equiv(\beta \wedge \alpha) \quad \text { commutativity of } \wedge \\ (\alpha \vee \beta) & \equiv(\beta \vee \alpha) \quad \text { commutativity of } \vee \\ ((\alpha \wedge \beta) \wedge \gamma) & \equiv(\alpha \wedge(\beta \wedge \gamma)) \quad \text { associativity of } \wedge \\ ((\alpha \vee \beta) \vee \gamma) & \equiv(\alpha \vee(\beta \vee \gamma)) \quad \text { associativity of } \vee \\ \neg(\neg \alpha) & \equiv \alpha \quad \text { double-negation elimination } \\ (\alpha \Rightarrow \beta) & \equiv(\neg \beta \Rightarrow \neg \alpha) \quad \text { contraposition } \\ (\alpha \Rightarrow \beta) & \equiv(\neg \alpha \vee \beta) \quad \text { implication elimination } \\ (\alpha \Leftrightarrow \beta) & \equiv((\alpha \Rightarrow \beta) \wedge(\beta \Rightarrow \alpha)) \quad \text { biconditional elimination } \\ \neg(\alpha \wedge \beta) & \equiv(\neg \alpha \vee \neg \beta) \quad \text { De Morgan } \\ \neg(\alpha \vee \beta) & \equiv(\neg \alpha \wedge \neg \beta) \quad \text { De Morgan } \\ (\alpha \wedge(\beta \vee \gamma)) & \equiv((\alpha \wedge \beta) \vee(\alpha \wedge \gamma)) \quad \text { distributivity of } \wedge \text { over } \vee \\ (\alpha \vee(\beta \wedge \gamma)) & \equiv((\alpha \vee \beta) \wedge(\alpha \vee \gamma)) \quad \text { distributivity of } \vee \text { over } \wedge \end{aligned}$

Las ecuaciones anteriores muestran todas las equivalencias lógicas que se pueden utilizar como reglas de inferencia. La equivalencia para la eliminación bicondicional, por ejemplo, produce las dos reglas de inferencia.

$\frac{\alpha \Leftrightarrow \beta}{(\alpha \Rightarrow \beta) \wedge(\beta \Rightarrow \alpha)} \quad \text { and } \quad \frac{(\alpha \Rightarrow \beta) \wedge(\beta \Rightarrow \alpha)}{\alpha \Leftrightarrow \beta}$

Algunas reglas de inferencia no funcionan en ambas direcciones de la misma manera. No podemos, por ejemplo, ejecutar Modus Ponens en la dirección inversa para obtener $\alpha \Rightarrow \beta$ y $\alpha \text{ from } \beta$ .

Veamos cómo se pueden aplicar estas equivalencias y reglas de inferencia en el entorno wumpus. Comenzamos con la base de conocimientos que incluye R1 a R5 y demostramos cómo establecer, $\neg P_{1,2}$ es decir, que [1,2] no incluye pozos. Para generar R6, primero aplicamos eliminación bicondicional a R2:

$R_{6}: \quad\left(B_{1,1} \Rightarrow\left(P_{1,2} \vee P_{2,1}\right)\right) \wedge\left(\left(P_{1,2} \vee P_{2,1}\right) \Rightarrow B_{1,1}\right)$

Después de eso, aplicamos Y-Eliminación en R6 para obtener $R_{7}: \quad\left(\left(P_{1,2} \vee P_{2,1}\right) \Rightarrow B_{1,1}\right)$

Para contrapositivos, la equivalencia lógica produce $R_{8}: \quad\left(\neg B_{1,1} \Rightarrow \neg\left(P_{1,2} \vee P_{2,1}\right)\right)$

Con R8 y el percepto $R_{4} \text { (i.e., } \neg B_{1,1} \text { ) }$ , ahora podemos aplicar Modus Ponens para obtener $R_{9}: \quad \neg\left(P_{1,2} \vee P_{2,1}\right)$ .

Finalmente, usamos la regla de De Morgan para llegar a la siguiente conclusión: $R_{10}: \quad \neg P_{1,2} \wedge \neg P_{2,1}$

Es decir, ni [1,2] ni [2,1] tienen hoyo en ellos.

Encontramos esta prueba a mano, pero cualquiera de las técnicas de búsqueda puede usarse para producir una secuencia de pasos similar a una prueba. Todo lo que tenemos que hacer ahora es definir un problema de prueba:

Estado Inicial: el punto de partida del conocimiento.
Acciones: el conjunto de acciones está formado por todas las reglas de inferencia que se han aplicado a todas las oraciones que se ajustan a la mitad superior de la regla de inferencia.
Consecuencias: Agregar la declaración a la parte inferior de la regla de inferencia es el resultado de una acción.
Objetivo: El objetivo es llegar a un estado que contenga la frase que estamos tratando de verificar.

Como resultado, buscar pruebas es una alternativa viable a contar modelos.

Publicación traducida automáticamente

Artículo escrito por Mohit Gupta_OMG 🙂 y traducido por Barcelona Geeks. The original can be accessed here. Licence: CCBY-SA

Inferencias en la demostración del teorema proposicional

Deja una respuesta Cancelar la respuesta