Hasta aquí hemos visto la forma estándar de la LPO, existe otra forma de representación en lógica llamada forma clausal. La forma clausal es más sencilla que la estándar, aunque esta última es más natural. La propiedad importante de la forma clausal es que: un conjunto de wff en forma estándar es inconsistente si y sólo si el conjunto de cláusulas correspondiente es inconsistente. Cuando nos referimos al conjunto de cláusulas correspondiente nos referimos a aquellas convertidas a partir de la forma estándar. En realidad la forma clausal es un subconjunto restringido de la forma estándar pero que cuenta con algoritmos eficientes para razonar sobre ellas.
Definamos entonces que entendemos por cláusulas. Para ello primero debemos dar la definición de fórmula atómica y de literal:
-
Fórmula Atómica:
siendo los ti términos y 
un símbolo predicativo, es una fórmula atómica
-
Literal: Sea F una fórmula atómica, entonces F y -F son literales. Es decir los literales son las formulas atómicas y su negación.
Y ahora pasamos a la definición de cláusula:
Cláusula: Es una disyunción finita de literales. Puede consistir de un solo literal en cuyo caso se llama cláusula unitaria
La representación en forma clausal consiste de un conjunto de cláusulas, es decir un conjunto de disyunciones. Cuando hablamos de disyunción o conjunción de literales podemos hablar de forma normal conjuntiva y forma normal disyuntiva. La primera es una conjunción de disyunciones y la segunda es una disyunción de conjunciones. En el caso de la forma normal conjuntiva podemos decir que es una conjunción de cláusulas.
Sea C1, C2,…,Cn cláusulas (es decir C1 es de la forma L1 v L2 v L3…vLm ) entonces la forma normal conjuntiva son expresiones como: C1 ^C2 …^Cn
Así como vimos el modus ponens como regla de inferencia existen otras reglas, una de las cuales es la Resolución. En el cálculo proposicional la resolución se define como sigue:
La notación significa que dadas las premisas (sobre la línea) se tiene la conclusión (bajo la línea). Si tenemos en cuenta la equivalencia entre la implicación y el conector Úentonces esta regla es equivalente al teorema de la transitividad de la implicación. Para verlo expresemos las fórmulas con implicación lo que queda como: dado -A ->B, B->C entonces se deduce: -A->C.
Ahora pasaremos a expresar la resolución en el cálculo de predicados, el cual cuenta con variables. Por lo que previamente debemos tratar con los conceptos de sustitución y unificación.
Sustitución: Una sustitución es un conjunto finito de pares {x1/,t1….xn/tn}donde cada xi es una variable y ti es un término tal que xi ¹ti y xi ¹xj si i ¹j. La sustitución vacía la notamos e
Es posible aplicar una sustitución a un término o a una fórmula, sea b una sustitución y F una fórmula la aplicación de una sustitución a una fórmula, que notamos Fb es la fórmula obtenida por reemplazar simultáneamente toda ocurrencia de cada xi en F por ti. Fb se llama instanciación de F o es una instancia de F.
Unificador: sean t1 y t2 términos. Una sustitución q tal que t1q = t2q se dice que es un unificador. Es decir, un unificador es una sustitución tal que al aplicarla a dos términos hace a estos sintácticamente iguales.
A su vez, es posible definir el concepto de unificador más general , un unificador q es más general que otro b, si existe una sustitución a tal que b= qa. Intuitivamente decimos es que es posible componer (en el mismo sentido que la composición de funciones) un unificador con algún otro para obtener el menos general.
Unificador más general (mgu – most general unifier): Un unificador 
se dice que es el mgu de un par de términos si y solo si es más general que cualquier otro unificador de dichos términos. Se puede probar que el mgu es único salvo cambio de nombre en variables.
Podemos definir la resolución generalizada para más de una disyunción de la siguiente manera:
Si es el mgu de los literales 
entonces:
La línea de abajo es la aplicación del mgu a toda la disyunción.
Hemos dicho que las fórmulas en forma estándar tienen una equivalencia en forma clausal. Esta equivalencia es un conjunto de cláusulas (fórmulas en forma clausal) que se consideran en conjunción implícita. Es decir es como si todas las cláusulas estuvieran unidas por conjunción. Posteriormente daremos el método para transformar una sentencia en forma estándar a forma clausal. Si vemos la resolución generalizada vemos que cada una de las premisas es una cláusula.
La ventaja de trabajar con resolución es que es un método de inferencia correcto y completo. Lo que estamos diciendo es que si encontramos una demostración de algo entonces esto es válido, y además que si existe una demostración es posible encontrarla.
Las cláusulas de las cuales se deriva la conclusión mediante resolución se denominan cláusulas padres y el resultado como resolvente de ellas.
Si tenemos un conjunto de cláusulas S en el cual si todas son verdaderas entonces cualquier cláusula deducible de ellas es verdadera, estamos diciendo que es imposible deducir la cláusula vacía o falsa (
).
Si queremos demostrar que alguna cláusula F es consecuencia de un conjunto de cláusulas S (consistente) entonces si agregamos ØF al conjunto de cláusulas y mediante resolución llegamos a entonces estamos refutando -F, por lo cual F se deduce del conjunto de cláusulas. Esto se llama refutación por resolución y es un mecanismo ampliamente usado en probadores de teoremas.