A naïve implementation of sequent calculus.

sequent_calculus.hs

module Calculus where

import Control.Monad (liftM2)
import Data.List     (sort, permutations, nub)

import Data.Char     (chr)
import Debug.Trace

data Formula  = Formula Int
              | Not Formula
              | Or  Formula Formula
              deriving (Eq, Ord)

instance Show Formula where
  show (Formula x) = [chr (x + 96)]
  show (Not x)     = "¬" ++ show x
  show (Or  x y)   = show x ++ " ∨ " ++ show y

data Sequent = Sequent {
    antecedents :: [Formula]
  , succedent   :: Formula
  } deriving (Eq, Ord)

instance Show Sequent where
  show (Sequent as s) = show s ++ " -| " ++ show as

-- Connective Rules
proofByCase :: Sequent -> Sequent -> [Sequent]
proofByCase (Sequent (a1:as1) s1) (Sequent ((Not a2):as2) s2)
  | a1 == a2 && as1 == as2 && s1 == s2 = [Sequent as1 s1]
proofByCase _ _ = []

contradiction :: Sequent -> Sequent -> [Sequent]
contradiction (Sequent ((Not a1):as1) s1) (Sequent ((Not a2):as2) (Not s2))
  | a1 == a2 && as1 == as2 && s1 == s2 = [Sequent as1 a1]
contradiction _ _ = []

orAntecedent :: Sequent -> Sequent -> [Sequent]
orAntecedent (Sequent (a1:as1) s1) (Sequent (a2:as2) s2)
  | a1 == a2     = []
  | as1 == as2 && s1 == s2 = [Sequent ((Or a1 a2):as1) s1]
orAntecedent _ _ = []

orSuccedent :: Sequent -> [Formula] -> [Sequent]
orSuccedent (Sequent xs s) fs = Sequent xs <$> ss'
  where ss' = map (Or s) fs ++ map (flip Or s) fs

-- Structure Rules
antecedent :: [Sequent] -> [Formula] -> [Sequent]
antecedent ss fs = concatMap gen ss
  where gen (Sequent as s) = map (flip Sequent s . (: as)) fs

assumption :: [Sequent] -> [Formula] -> [Sequent]
assumption ss fs = concatMap gen ss ++ primitives
  where gen (Sequent as _) = map (Sequent =<< (: as)) fs
        primitives         = [Sequent [f] f | f <- fs]

derive :: [Formula] -> [Sequent] -> [Sequent]
derive atoms ss = let
  derived  = concatMap (f1 $) [proofByCase, contradiction, orAntecedent]
          ++ concatMap (f2 $) [orSuccedent]
          ++ concatMap (f3 $) [antecedent, assumption]
          ++ ss
  derived' = concatMap mkPerm derived where
    mkPerm s = [Sequent as (succedent s) | as <- permutations $ antecedents s]
  in filter customFilter $ removeDuplicates derived'
  where
    fs = removeDuplicates $ map Not fs' ++ fs'
      where fs' = atoms ++ concatMap extractFormulas ss

    f1 :: (Sequent -> Sequent -> [Sequent]) -> [Sequent]
    f1 rule = concat [rule x y | x <- ss, y <- ss, x /= y]
    f2 :: (Sequent -> [Formula] -> [Sequent]) -> [Sequent]
    f2 rule = concat [rule s fs | s <- ss]
    f3 :: ([Sequent] -> [Formula] -> [Sequent]) -> [Sequent]
    f3 rule = rule ss fs

    customFilter (Sequent as s)
      | length as > 3 = False
      | nub as /= as  = False
      | (not . null) $ filter (> 3) $ map formulaSize (s:as) = False
      | otherwise     = True

removeDuplicates :: (Ord a) => [a] -> [a]
removeDuplicates = rmdup . sort where
  rmdup (x1:x2:xs)
    | x1 == x2  = rmdup (x1:xs)
    | otherwise = x1:(rmdup (x2:xs))
  rmdup x = x

extractFormulas :: Sequent -> [Formula]
extractFormulas = liftM2 (:) succedent antecedents

extractAtoms :: Sequent -> [Formula]
extractAtoms = concatMap unfold . extractFormulas where
  unfold (Formula x) = [Formula x]
  unfold (Not x)     = unfold x
  unfold (Or x y)    = unfold x ++ unfold y

formulaSize :: Formula -> Int
formulaSize (Formula _) = 1
formulaSize (Not x)     = 1 + formulaSize x
formulaSize (Or x y)    = max (formulaSize x) (formulaSize y)

check :: [Sequent] -> Sequent -> Bool
check premises target = check' premises where
  atoms = removeDuplicates $ concatMap extractAtoms (target:premises)
  check' derived = let
    derived' = derive atoms derived
    in if target `elem` derived
       then True
       else if length derived == length derived'
            then trace (show $ length derived') False
            else trace (show $ length derived') $ check' derived'

varphi :: Formula
varphi = Formula 1
psi    :: Formula
psi    = Formula 2