{- |
Description: Resolution rule
Copyright: Copyright (C) 2023 Yoo Chung
License: GPL-3.0-or-later
Maintainer: dev@chungyc.org

Some solutions to "Problems.P53" of Ninety-Nine Haskell "Problems".
-}
module Solutions.P53 (isTheorem) where

import           Control.Monad  (guard)
import           Data.Set       (Set)
import qualified Data.Set       as Set
import           Problems.Logic (Formula (..))
import           Problems.P52   (toConjunctiveNormalForm)

-- | Determines whether the formula is valid given the axioms.
isTheorem :: [Formula] -> Formula -> Bool
isTheorem :: [Formula] -> Formula -> Bool
isTheorem [Formula]
axioms Formula
conjecture = Set (Set Formula) -> Bool
refute (Set (Set Formula) -> Bool) -> Set (Set Formula) -> Bool
forall a b. (a -> b) -> a -> b
$ (Set Formula -> Bool) -> Set (Set Formula) -> Set (Set Formula)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set Formula -> Bool) -> Set Formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Formula -> Bool
isTautology) Set (Set Formula)
clauses
  where axioms' :: [Formula]
axioms' = (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
purify [Formula]
axioms
        conjecture' :: Formula
conjecture' = Formula -> Formula
purify Formula
conjecture
        aggregate :: Formula
aggregate = [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
Complement Formula
conjecture' Formula -> [Formula] -> [Formula]
forall a. a -> [a] -> [a]
: [Formula]
axioms'
        clauses :: Set (Set Formula)
clauses = Formula -> Set (Set Formula)
toClauses (Formula -> Set (Set Formula)) -> Formula -> Set (Set Formula)
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
toConjunctiveNormalForm Formula
aggregate

-- | Replace all values and empty clauses in a formula with
-- equivalent expressions which have no values and no empty clauses.
purify :: Formula -> Formula
purify :: Formula -> Formula
purify (Value Bool
True)   = Formula
true
purify (Value Bool
False)  = Formula
false
purify f :: Formula
f@(Variable String
_) = Formula
f
purify (Complement Formula
f) = Formula -> Formula
Complement (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula
purify Formula
f
purify (Disjoin [])   = Formula
false
purify (Conjoin [])   = Formula
true
purify (Disjoin [Formula]
fs)   = [Formula] -> Formula
Disjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
purify [Formula]
fs
purify (Conjoin [Formula]
fs)   = [Formula] -> Formula
Conjoin ([Formula] -> Formula) -> [Formula] -> Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
purify [Formula]
fs

-- An expression which is always true; for use with purify.
true :: Formula
true :: Formula
true = [Formula] -> Formula
Disjoin [ Formula
x, Formula -> Formula
Complement Formula
x ]
  -- An arbitrary variable.
  --
  -- It does not matter whether the rest of the formula
  -- uses this variable or not.  Either way, the rest
  -- of the formula does not affect the result of this
  -- expression, and vice versa.
  where x :: Formula
x = String -> Formula
Variable String
"X"

-- An expression which is always false; for use with purify.
false :: Formula
false :: Formula
false = [Formula] -> Formula
Conjoin [ Formula
x, Formula -> Formula
Complement Formula
x ]
  -- An arbitrary variable.
  --
  -- It does not matter whether the rest of the formula
  -- uses this variable or not.  Either way, the rest
  -- of the formula does not affect the result of this
  -- expression, and vice versa.
  where x :: Formula
x = String -> Formula
Variable String
"X"

-- | Transform a formula in conjunctive normal form into a set of clauses,
-- with each clause being a set of literals.
toClauses :: Formula -> Set (Set Formula)
toClauses :: Formula -> Set (Set Formula)
toClauses (Conjoin [Formula]
fs) = [Set Formula] -> Set (Set Formula)
forall a. Ord a => [a] -> Set a
Set.fromList ([Set Formula] -> Set (Set Formula))
-> [Set Formula] -> Set (Set Formula)
forall a b. (a -> b) -> a -> b
$ (Formula -> Set Formula) -> [Formula] -> [Set Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Set Formula
toSet [Formula]
fs
toClauses Formula
f            = String -> Set (Set Formula)
forall a. HasCallStack => String -> a
error (String -> Set (Set Formula)) -> String -> Set (Set Formula)
forall a b. (a -> b) -> a -> b
$ String
"not conjunctive normal form: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Show a => a -> String
show Formula
f

-- | Transform a disjunction of literals into a set of literals representing a clause.
toSet :: Formula -> Set Formula
toSet :: Formula -> Set Formula
toSet (Disjoin [Formula]
fs) = [Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList [Formula]
fs
toSet Formula
f            = String -> Set Formula
forall a. HasCallStack => String -> a
error (String -> Set Formula) -> String -> Set Formula
forall a b. (a -> b) -> a -> b
$ String
"not part of conjunctive normal form: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Show a => a -> String
show Formula
f

-- | Refute the given formula in conjunctive normal form.
-- I.e., derive a false statement, which means contradiction.
refute :: Set (Set Formula) -> Bool
refute :: Set (Set Formula) -> Bool
refute Set (Set Formula)
clauses
  | Maybe (Set Formula)
Nothing <- Maybe (Set Formula)
resolved = Bool
False
  | Just Set Formula
c <- Maybe (Set Formula)
resolved, Set Formula -> Bool
forall a. Set a -> Bool
Set.null Set Formula
c = Bool
True
  | Just Set Formula
c <- Maybe (Set Formula)
resolved = Set (Set Formula) -> Bool
refute (Set (Set Formula) -> Bool) -> Set (Set Formula) -> Bool
forall a b. (a -> b) -> a -> b
$ Set Formula -> Set (Set Formula) -> Set (Set Formula)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set Formula
c Set (Set Formula)
clauses
  where resolved :: Maybe (Set Formula)
resolved = Set (Set Formula) -> [Match] -> Maybe (Set Formula)
resolve Set (Set Formula)
clauses ([Match] -> Maybe (Set Formula)) -> [Match] -> Maybe (Set Formula)
forall a b. (a -> b) -> a -> b
$ Set (Set Formula) -> [Match]
matches Set (Set Formula)
clauses

-- | Represents two clauses, each of which has a literal and its complement.
-- Each pair is the matching literal and the clause containing the literal.
type Match = ((Formula, Set Formula), (Formula, Set Formula))

-- | Find two clauses which match, in that one has a literal
-- whose complement is contained in the other literal.
matches :: Set (Set Formula) -> [Match]
matches :: Set (Set Formula) -> [Match]
matches Set (Set Formula)
clauses = do
  let clauseList :: [Set Formula]
clauseList = Set (Set Formula) -> [Set Formula]
forall a. Set a -> [a]
Set.toList Set (Set Formula)
clauses
  Set Formula
clause <- [Set Formula]
clauseList
  Set Formula
clause' <- [Set Formula]
clauseList
  Formula
x <- Set Formula -> [Formula]
forall a. Set a -> [a]
Set.toList Set Formula
clause
  let x' :: Formula
x' = Formula -> Formula
complement Formula
x
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Formula -> Set Formula -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Formula
x' Set Formula
clause'
  Match -> [Match]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Formula
x, Set Formula
clause), (Formula
x', Set Formula
clause'))

-- | Apply the resolution rule and return the result
-- if it is not already in the set of axioms.
resolve :: Set (Set Formula) -> [Match] -> Maybe (Set Formula)
resolve :: Set (Set Formula) -> [Match] -> Maybe (Set Formula)
resolve Set (Set Formula)
clauses [Match]
matchings
  | [] <- [Match]
ms = Maybe (Set Formula)
forall a. Maybe a
Nothing
  | (Match
m:[Match]
_) <- [Match]
ms = Set Formula -> Maybe (Set Formula)
forall a. a -> Maybe a
Just (Set Formula -> Maybe (Set Formula))
-> Set Formula -> Maybe (Set Formula)
forall a b. (a -> b) -> a -> b
$ Match -> Set Formula
forall {a}. Ord a => ((a, Set a), (a, Set a)) -> Set a
merge Match
m
  where ms :: [Match]
ms = (Match -> Bool) -> [Match] -> [Match]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Match -> Bool
ignored [Match]
matchings
        merge :: ((a, Set a), (a, Set a)) -> Set a
merge ((a
v, Set a
c), (a
v', Set a
c')) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
v (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
v' (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Set a
c Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set a
c'
        ignored :: Match -> Bool
ignored Match
m = let c :: Set Formula
c = Match -> Set Formula
forall {a}. Ord a => ((a, Set a), (a, Set a)) -> Set a
merge Match
m
                    in Set Formula
c Set Formula -> Set (Set Formula) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Set Formula)
clauses Bool -> Bool -> Bool
|| Set Formula -> Bool
isTautology Set Formula
c

-- | Whether the given clause is a trivial tautology
-- due to having a literal and its complement in the disjunction.
isTautology :: Set Formula -> Bool
isTautology :: Set Formula -> Bool
isTautology Set Formula
s = (Formula -> Bool) -> Set Formula -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Formula
x -> Formula -> Formula
complement Formula
x Formula -> Set Formula -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Formula
s) Set Formula
s

-- | Returns the complement of the given formula.
-- Ensures that literals remain literals.
complement :: Formula -> Formula
complement :: Formula -> Formula
complement (Complement Formula
x) = Formula
x
complement Formula
x              = Formula -> Formula
Complement Formula
x