Resolución (lógica)

Resolución solamente funciona cuando se escriben las proposiciones en términos de premisas que constan solamente de disyunciones de literales. Puesto que toda proposición lógica se puede escribir en términos de disyunciones, conjunciones y negaciones lo anterior no supone una limitación del método más allá de transformar proposiciones lógicas. Las proposiciones escritas en esta forma se les denomina cláusulas.

La regla es bastante sencilla y un ejemplo muestra el razonamiento detrás de ella, de las siguientes dos oraciones: 'Juan va a al cine o Julia va a patinar' y 'Juan no va el cine o Jorge juega fútbol' podemos deducir la siguiente oración 'Julia va a patinar o Jorge juega fútbol' la razón es que puesto que Juan no puede al mismo tiempo ir y no ir al cine, para que las disyunciones anteriores sean ciertas se debe de cumplir alguna de las dos proposiciones: 'Julia va a patinar' o 'Jorge juega fútbol' o ambas.

En general esta regla se escribe de la siguiente forma:

${\displaystyle {\frac {p_{1}\lor \ldots \vee p_{i}\vee \ldots \lor p_{n},\quad q_{1}\lor \ldots \vee q_{j}\vee \ldots \lor q_{m}}{p_{1}\lor \ldots \lor p_{i-1}\lor p_{i+1}\lor \ldots \lor p_{n}\lor q_{1}\lor \ldots \lor q_{j-1}\lor q_{j+1}\lor \ldots \lor q_{m}}}}$

donde:

${\displaystyle \forall i\in \left\lbrace 1,2,\ldots ,n\right\rbrace p_{i}}$ es un literal

${\displaystyle \forall j\in \left\lbrace 1,2,\ldots ,m\right\rbrace q_{j}}$ es un literal

y ${\displaystyle p_{i}}$ es la negación (complementario) de ${\displaystyle q_{j}}$