{- |
Description: Resolution rule
Maintainer: dev@chungyc.org

Part of Ninety-Nine Haskell "Problems".  Some solutions are in "Solutions.P53".
-}
module Problems.P53 (isTheorem, Formula (..)) where

import           Problems.Logic (Formula (..))
import qualified Solutions.P53  as Solution

{- | In propositional logic, if a formula $$X$$ is always true
when a set of axioms $$\mathrm{S}$$ are true,
then $$X$$ is said to be /valid/ given $$\mathrm{S}$$.

The /resolution rule/ is an inference rule in propositional logic
where two clauses with complementary literals can be merged to produce
another clause.  Specifically, if clauses $$x \vee a_1 \vee \ldots \vee a_m$$
and $$\neg x \vee b_1 \vee \ldots \vee b_n$$ are true, then
the clause $$a_1 \vee \ldots \vee a_m \vee b_1 \vee \ldots \vee b_n$$
must also be true.  This is commonly expressed as

$x \vee a_1 \vee \ldots \vee a_m \hspace{2em} \neg x \vee b_1 \vee \ldots \vee b_n \above 1pt a_1 \vee \ldots \vee a_m \vee b_1 \vee \ldots \vee b_n$

The resolution rule can be used with conjunctive normal forms to prove whether or not
a given formula $$X$$ is valid given a set of axioms $$\mathrm{S}$$.
It is a proof by contradiction, and the procedure is as follows:

1.  Conjunctively connect the formulas in $$\mathrm{S}$$
and the /negation/ of $$X$$ into a single formula $$Y$$.

For example, if the axioms are $$x$$ and $$y$$, and
the given formula is $$z$$, then $$Y$$ would be $$x \wedge y \wedge \neg z$$.

*   Do not apply the resolution rule to the values of true and false.
If $$Y$$ contains raw true or false values,
transform $$Y$$ into a form which contains none.

2.  Convert $$Y$$ into conjunctive normal form; see "Problems.P52".

3.  If there are two clauses for which the resolution rule can be applied,
add the new clause to $$Y$$ and repeat until an empty clause is inferred
or if no new clauses can be added.  Filter out tautologies, i.e.,
clauses which will always be true because it contains both a variable
and its logical complement.

*   If the empty clause has been inferred, then false has been inferred
from $$Y$$.  I.e., there is a contradiction, so $$X$$ must have been
valid given the axioms $$\mathrm{S}$$.

*   If no more clauses can be inferred, then $$X$$ cannot be inferred to be valid.

Given a list of axioms and a formula, use the resolution rule to determine
whether the formula is valid given the axioms.

=== Examples

When $$x \wedge y \wedge z$$ is true, then obviously $$x \vee y$$ is true, so

>>> :{
isTheorem
[ Variable "X", Variable "Y", Variable "Z" ] $Disjoin [ Variable "X", Variable "Y" ] :} True When $$x \to y$$ and $$y \to z$$, or equivalently $$\neg x \vee y$$ and $$\neg y \vee z$$, then it is also the case that $$x \to z$$, so >>> :{ isTheorem [ Disjoin [ Complement$ Variable "X", Variable "Y" ]
, Disjoin [ Complement $Variable "Y", Variable "Z" ] ]$
Disjoin [ Complement $Variable "X", Variable "Z" ] :} True Just because $$x$$ is true does not mean that $$y$$ is true, so >>> isTheorem [ Variable "X" ]$ Variable "Y"
False

If there is a contradiction, then everything is both true and false, so

>>> isTheorem [ Variable "X", Complement $Variable "X" ]$ Value False
True
-}
isTheorem :: [Formula] -> Formula -> Bool
isTheorem :: [Formula] -> Formula -> Bool
isTheorem = [Formula] -> Formula -> Bool
Solution.isTheorem