En los ejercicios de deducción natural que se proponen en este sitio, se puede interactuar con la aplicación para tratar de hacer la demostración usando las reglas adecuadas.
Una vez que aparezcan las premisas verás unos puntos suspensivos indicando que hace falta introducir alguna regla más para finalizar el ejercicio, mientras que si aparece \(qed\) (quod erat demonstrandum \(\equiv\) lo que se quería demostrar) indica que se ha completado el ejercicio con éxito.
Para introducir una regla nueva se debe introducir en el cuadro de texto de la izquierda y pulsar el botón Añadir Regla. Para ello debes tener en cuenta los siguientes atajos de teclado:
| Símbolo | Alternativa 1 | Alternativa 2 | Alternativa 3 | |
|---|---|---|---|---|
| Conjunción | \(\land\) | & | * | and |
| Disyunción | \(\lor\) | | | + | or |
| Negación | \(\lnot\) | ~ | – | not |
| Condicional | \(\to\) | -> | cond | |
| Bicondicional | \(\leftrightarrow\) | <-> | iif | bicond |
| Contradicción | \(\bot\) | F | false | falso |
Las reglas que se admiten son las siguientes:
| Símbolo | Texto a teclear | Explicación y fórmulas implicadas | |
|---|---|---|---|
| Introducción de la conjunción | \(\land \hbox{i} \; \hbox{a,b}\) | & i a,b | Fórmulas de las líneas «a» y «b» |
| Eliminación de la conjunción | \(\land \hbox{e}_{1} \; \hbox{a}\) \(\land \hbox{e}_{2} \; \hbox{a}\) | & e 1,a & e 2,a | Primer operando de la fórmula de la línea «a» Segundo operando de la fórmula de la línea «a» |
| Introducción de la doble negación | \(\lnot \lnot \hbox{i} \; \hbox{a}\) | – – i a | Fórmula de la línea «a» |
| Eliminación de la doble negación | \(\lnot \lnot \hbox{e} \; \hbox{a}\) | – – e a | Fórmula de la línea «a» |
| Eliminación del condicional | \(\to\hbox{e} \; \hbox{a,b}\) | -> e a,b | La fórmula de la línea «a» deber ser el antecedente de la fórmula «b» |
| Modus Tollens | \(\hbox{MT} \; \hbox{a,b}\) | MT a,b | La fórmula de la línea «a» debe ser el consecuente de la fórmula «b» |
| Introducción del condicional | \(\to\hbox{i} \; \hbox{a-b}\) | -> i a-b | La caja de supuesto empieza en la línea «a» y acaba en la «b» |
| Introducción de la disyunción | \(\lor \hbox{i}_{1} \; \hbox{a} \) \(\lor \hbox{i}_{2} \; \hbox{a} \) | | i 1,a | i 2,a | Se queda la fórmula «a» como primer operando de la disyunción Se queda la fórmula «a» como segundo operando de la disyunción En ambos casos se debe usar el cuadro de texto de la derecha para introducir una fórmula |
| Eliminación de la disyunción | \(\lor \hbox{e} \; \hbox{a,b-c,d-e}\) | | e a,b-c,d-e | Se elimina la disyunción de la línea «a» Las cajas de supuesto implicadas son la que empieza en «b» y termina en «c» y la que empieza en «d» y termina en «e» |
| Copia | \(\hbox{copia} \; \hbox{a}\) | C a copia a copy a | Se copia la fórmula de la línea «a» |
| Eliminación de lo falso | \(\bot \hbox{e} \; \hbox{a} \) | F a false a falso a | La fórmula «a» debe ser una contradicción Se debe usar el cuadro de texto de la derecha para introducir una fórmula |
| Eliminación de la negación | \(\lnot \hbox{e} \; \hbox{a,b}\) | – e a,b | Las fórmulas «a» y «b» deben ser negadas la una de la otra |
| Introducción de la negación | \(\lnot \hbox{i} \; \hbox{a-b}\) | – i a-b | La caja de supuesto empieza en la línea «a» y acaba en la «b» La caja de supuesto debe terminar en contradicción |
| Reducción al absurdo | \(\hbox{RAA} \; \hbox{a-b}\) | RAA a-b | La caja de supuesto empieza en la línea «a» y acaba en la «b» La caja de supuesto debe terminar en contradicción |
| Ley del tercio excluido | \(\hbox{LEM}\) | LEM | Se debe usar el cuadro de texto de la derecha para introducir una fórmula \(F\) La fórmula resultante será \(F \lor \lnot F\) |
| Eliminación del bicondicional | \(\leftrightarrow \hbox{e}_{1} \; \hbox{a}\) \(\leftrightarrow \hbox{e}_{1} \; \hbox{a}\) | <-> e 1,a <-> e 2,a | Primer operando de la fórmula de la línea «a» Segundo operando de la fórmula de la línea «a» |
| Introducción del bicondicional | \(\leftrightarrow \hbox{i} \; \hbox{a,b}\) | <-> i a,b | Las fórmulas de las líneas «a» y «b» deben ser de la forma \(F \to G\) y \(G \to F\) |
De tal forma que si queremos añadir al ejercicio la regla de introducción de la conjunción entre la fórmula de la línea 1 y la fórmula de la línea 2 deberemos teclear «& i 1,2» aunque hay flexibilidad en cuanto a los operadores lógicos y los espacios (cuidado, los guiones y las comas sí hay que respetarlos). Así que también valdría «and i1,2».
En caso de querer abrir una caja de supuesto habría que teclear la fórmula en el cuadro de texto de la derecha y pulsar el botón Abrir Supuesto. Por cierto, en este segundo cuadro de texto se puede teclear la fórmula deseada usando los mismos atajos de teclado que en las reglas. Así que si queremos introducir la fórmula \(p \land q \to \lnot r \lor q\) habría que teclear «p & q -> -r | q» pero también valdría «p and q cond not r or q». Las variables lógicas se representan por literales formadas por las letras, por lo que no valen «x0» y «y1», por ejemplo, como variables.
Si lo que queremos es cerrar una caja de supuesto sólo tendremos que pulsar el botón Cerrar Supuesto.
Los botones Deshacer y Reiniciar eliminan la última regla o todas las que se han introducido respectivamente.