{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE CPP #-}

{-|
Module       : ATP.FirstOrder.Derivation
Description  : Derivations in first-order logic.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental
-}

module ATP.FirstOrder.Derivation (
  -- * Proofs
  Rule(..),
  RuleName(..),
  ruleName,
  Inference(..),
  antecedents,
  Contradiction(..),
  Sequent(..),
  Derivation(..),
  addSequent,
  breadthFirst,
  labeling,
  Refutation(..),
  Solution(..)
) where

import Data.Foldable (toList)
import Data.Function (on)
import Data.List (sortBy)
import qualified Data.Map as M (fromList, insert, toList)
import Data.Map (Map, (!))
#if !MIN_VERSION_base(4, 11, 0)
import Data.Semigroup (Semigroup)
#endif
import Data.String (IsString(..))
import Data.Text (Text)

import ATP.FirstOrder.Core


-- * Proofs

-- | The inference rule.
data Rule f
  = Axiom
  | Conjecture
  | NegatedConjecture  f
  | Flattening         f
  | Skolemisation      f
  | EnnfTransformation f
  | NnfTransformation  f
  | Clausification     f
  | TrivialInequality  f
  | Superposition         f f
  | Resolution            f f
  | Paramodulation        f f
  | SubsumptionResolution f f
  | ForwardDemodulation   f f
  | BackwardDemodulation  f f
  | AxiomOfChoice
  | Unknown        [f]
  | Other RuleName [f]
  deriving (Int -> Rule f -> ShowS
[Rule f] -> ShowS
Rule f -> String
(Int -> Rule f -> ShowS)
-> (Rule f -> String) -> ([Rule f] -> ShowS) -> Show (Rule f)
forall f. Show f => Int -> Rule f -> ShowS
forall f. Show f => [Rule f] -> ShowS
forall f. Show f => Rule f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rule f] -> ShowS
$cshowList :: forall f. Show f => [Rule f] -> ShowS
show :: Rule f -> String
$cshow :: forall f. Show f => Rule f -> String
showsPrec :: Int -> Rule f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> Rule f -> ShowS
Show, Rule f -> Rule f -> Bool
(Rule f -> Rule f -> Bool)
-> (Rule f -> Rule f -> Bool) -> Eq (Rule f)
forall f. Eq f => Rule f -> Rule f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rule f -> Rule f -> Bool
$c/= :: forall f. Eq f => Rule f -> Rule f -> Bool
== :: Rule f -> Rule f -> Bool
$c== :: forall f. Eq f => Rule f -> Rule f -> Bool
Eq, Eq (Rule f)
Eq (Rule f)
-> (Rule f -> Rule f -> Ordering)
-> (Rule f -> Rule f -> Bool)
-> (Rule f -> Rule f -> Bool)
-> (Rule f -> Rule f -> Bool)
-> (Rule f -> Rule f -> Bool)
-> (Rule f -> Rule f -> Rule f)
-> (Rule f -> Rule f -> Rule f)
-> Ord (Rule f)
Rule f -> Rule f -> Bool
Rule f -> Rule f -> Ordering
Rule f -> Rule f -> Rule f
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f. Ord f => Eq (Rule f)
forall f. Ord f => Rule f -> Rule f -> Bool
forall f. Ord f => Rule f -> Rule f -> Ordering
forall f. Ord f => Rule f -> Rule f -> Rule f
min :: Rule f -> Rule f -> Rule f
$cmin :: forall f. Ord f => Rule f -> Rule f -> Rule f
max :: Rule f -> Rule f -> Rule f
$cmax :: forall f. Ord f => Rule f -> Rule f -> Rule f
>= :: Rule f -> Rule f -> Bool
$c>= :: forall f. Ord f => Rule f -> Rule f -> Bool
> :: Rule f -> Rule f -> Bool
$c> :: forall f. Ord f => Rule f -> Rule f -> Bool
<= :: Rule f -> Rule f -> Bool
$c<= :: forall f. Ord f => Rule f -> Rule f -> Bool
< :: Rule f -> Rule f -> Bool
$c< :: forall f. Ord f => Rule f -> Rule f -> Bool
compare :: Rule f -> Rule f -> Ordering
$ccompare :: forall f. Ord f => Rule f -> Rule f -> Ordering
$cp1Ord :: forall f. Ord f => Eq (Rule f)
Ord, a -> Rule b -> Rule a
(a -> b) -> Rule a -> Rule b
(forall a b. (a -> b) -> Rule a -> Rule b)
-> (forall a b. a -> Rule b -> Rule a) -> Functor Rule
forall a b. a -> Rule b -> Rule a
forall a b. (a -> b) -> Rule a -> Rule b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Rule b -> Rule a
$c<$ :: forall a b. a -> Rule b -> Rule a
fmap :: (a -> b) -> Rule a -> Rule b
$cfmap :: forall a b. (a -> b) -> Rule a -> Rule b
Functor, Rule a -> Bool
(a -> m) -> Rule a -> m
(a -> b -> b) -> b -> Rule a -> b
(forall m. Monoid m => Rule m -> m)
-> (forall m a. Monoid m => (a -> m) -> Rule a -> m)
-> (forall m a. Monoid m => (a -> m) -> Rule a -> m)
-> (forall a b. (a -> b -> b) -> b -> Rule a -> b)
-> (forall a b. (a -> b -> b) -> b -> Rule a -> b)
-> (forall b a. (b -> a -> b) -> b -> Rule a -> b)
-> (forall b a. (b -> a -> b) -> b -> Rule a -> b)
-> (forall a. (a -> a -> a) -> Rule a -> a)
-> (forall a. (a -> a -> a) -> Rule a -> a)
-> (forall a. Rule a -> [a])
-> (forall a. Rule a -> Bool)
-> (forall a. Rule a -> Int)
-> (forall a. Eq a => a -> Rule a -> Bool)
-> (forall a. Ord a => Rule a -> a)
-> (forall a. Ord a => Rule a -> a)
-> (forall a. Num a => Rule a -> a)
-> (forall a. Num a => Rule a -> a)
-> Foldable Rule
forall a. Eq a => a -> Rule a -> Bool
forall a. Num a => Rule a -> a
forall a. Ord a => Rule a -> a
forall m. Monoid m => Rule m -> m
forall a. Rule a -> Bool
forall a. Rule a -> Int
forall a. Rule a -> [a]
forall a. (a -> a -> a) -> Rule a -> a
forall m a. Monoid m => (a -> m) -> Rule a -> m
forall b a. (b -> a -> b) -> b -> Rule a -> b
forall a b. (a -> b -> b) -> b -> Rule a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Rule a -> a
$cproduct :: forall a. Num a => Rule a -> a
sum :: Rule a -> a
$csum :: forall a. Num a => Rule a -> a
minimum :: Rule a -> a
$cminimum :: forall a. Ord a => Rule a -> a
maximum :: Rule a -> a
$cmaximum :: forall a. Ord a => Rule a -> a
elem :: a -> Rule a -> Bool
$celem :: forall a. Eq a => a -> Rule a -> Bool
length :: Rule a -> Int
$clength :: forall a. Rule a -> Int
null :: Rule a -> Bool
$cnull :: forall a. Rule a -> Bool
toList :: Rule a -> [a]
$ctoList :: forall a. Rule a -> [a]
foldl1 :: (a -> a -> a) -> Rule a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Rule a -> a
foldr1 :: (a -> a -> a) -> Rule a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Rule a -> a
foldl' :: (b -> a -> b) -> b -> Rule a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Rule a -> b
foldl :: (b -> a -> b) -> b -> Rule a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Rule a -> b
foldr' :: (a -> b -> b) -> b -> Rule a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Rule a -> b
foldr :: (a -> b -> b) -> b -> Rule a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Rule a -> b
foldMap' :: (a -> m) -> Rule a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Rule a -> m
foldMap :: (a -> m) -> Rule a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Rule a -> m
fold :: Rule m -> m
$cfold :: forall m. Monoid m => Rule m -> m
Foldable, Functor Rule
Foldable Rule
Functor Rule
-> Foldable Rule
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Rule a -> f (Rule b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Rule (f a) -> f (Rule a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Rule a -> m (Rule b))
-> (forall (m :: * -> *) a. Monad m => Rule (m a) -> m (Rule a))
-> Traversable Rule
(a -> f b) -> Rule a -> f (Rule b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Rule (m a) -> m (Rule a)
forall (f :: * -> *) a. Applicative f => Rule (f a) -> f (Rule a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Rule a -> m (Rule b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Rule a -> f (Rule b)
sequence :: Rule (m a) -> m (Rule a)
$csequence :: forall (m :: * -> *) a. Monad m => Rule (m a) -> m (Rule a)
mapM :: (a -> m b) -> Rule a -> m (Rule b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Rule a -> m (Rule b)
sequenceA :: Rule (f a) -> f (Rule a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Rule (f a) -> f (Rule a)
traverse :: (a -> f b) -> Rule a -> f (Rule b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Rule a -> f (Rule b)
$cp2Traversable :: Foldable Rule
$cp1Traversable :: Functor Rule
Traversable)

-- | The name of an inference rule.
newtype RuleName = RuleName { RuleName -> Text
unRuleName :: Text }
  deriving (Int -> RuleName -> ShowS
[RuleName] -> ShowS
RuleName -> String
(Int -> RuleName -> ShowS)
-> (RuleName -> String) -> ([RuleName] -> ShowS) -> Show RuleName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RuleName] -> ShowS
$cshowList :: [RuleName] -> ShowS
show :: RuleName -> String
$cshow :: RuleName -> String
showsPrec :: Int -> RuleName -> ShowS
$cshowsPrec :: Int -> RuleName -> ShowS
Show, RuleName -> RuleName -> Bool
(RuleName -> RuleName -> Bool)
-> (RuleName -> RuleName -> Bool) -> Eq RuleName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RuleName -> RuleName -> Bool
$c/= :: RuleName -> RuleName -> Bool
== :: RuleName -> RuleName -> Bool
$c== :: RuleName -> RuleName -> Bool
Eq, Eq RuleName
Eq RuleName
-> (RuleName -> RuleName -> Ordering)
-> (RuleName -> RuleName -> Bool)
-> (RuleName -> RuleName -> Bool)
-> (RuleName -> RuleName -> Bool)
-> (RuleName -> RuleName -> Bool)
-> (RuleName -> RuleName -> RuleName)
-> (RuleName -> RuleName -> RuleName)
-> Ord RuleName
RuleName -> RuleName -> Bool
RuleName -> RuleName -> Ordering
RuleName -> RuleName -> RuleName
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RuleName -> RuleName -> RuleName
$cmin :: RuleName -> RuleName -> RuleName
max :: RuleName -> RuleName -> RuleName
$cmax :: RuleName -> RuleName -> RuleName
>= :: RuleName -> RuleName -> Bool
$c>= :: RuleName -> RuleName -> Bool
> :: RuleName -> RuleName -> Bool
$c> :: RuleName -> RuleName -> Bool
<= :: RuleName -> RuleName -> Bool
$c<= :: RuleName -> RuleName -> Bool
< :: RuleName -> RuleName -> Bool
$c< :: RuleName -> RuleName -> Bool
compare :: RuleName -> RuleName -> Ordering
$ccompare :: RuleName -> RuleName -> Ordering
$cp1Ord :: Eq RuleName
Ord, String -> RuleName
(String -> RuleName) -> IsString RuleName
forall a. (String -> a) -> IsString a
fromString :: String -> RuleName
$cfromString :: String -> RuleName
IsString)

-- | The name of the given inference rule.
--
-- >>> unRuleName (ruleName AxiomOfChoice)
-- "axiom of choice"
ruleName :: Rule f -> RuleName
ruleName :: Rule f -> RuleName
ruleName = \case
  Axiom{}                 -> RuleName
"axiom"
  Conjecture{}            -> RuleName
"conjecture"
  NegatedConjecture{}     -> RuleName
"negated conjecture"
  Flattening{}            -> RuleName
"flattening"
  Skolemisation{}         -> RuleName
"skolemisation"
  EnnfTransformation{}    -> RuleName
"ennf transformation"
  NnfTransformation{}     -> RuleName
"nnf transformation"
  Clausification{}        -> RuleName
"clausification"
  TrivialInequality{}     -> RuleName
"trivial inequality"
  Superposition{}         -> RuleName
"superposition"
  Resolution{}            -> RuleName
"resolution"
  Paramodulation{}        -> RuleName
"paramodulation"
  SubsumptionResolution{} -> RuleName
"subsumption resolution"
  ForwardDemodulation{}   -> RuleName
"forward demodulation"
  BackwardDemodulation{}  -> RuleName
"backward demodulation"
  AxiomOfChoice{}         -> RuleName
"axiom of choice"
  Unknown{}               -> RuleName
"unknown"
  Other RuleName
name [f]
_            -> RuleName
name

-- | A logical inference is an expression of the form
--
-- > A_1 ... A_n
-- > ----------- R,
-- >     C
--
-- where each of @A_1@, ... @A_n@ (called the 'antecedents'), and @C@
-- (called the 'consequent') are formulas and @R@ is an inference 'Rule'.
data Inference f = Inference {
  Inference f -> Rule f
inferenceRule :: Rule f,
  Inference f -> LogicalExpression
consequent :: LogicalExpression
} deriving (Int -> Inference f -> ShowS
[Inference f] -> ShowS
Inference f -> String
(Int -> Inference f -> ShowS)
-> (Inference f -> String)
-> ([Inference f] -> ShowS)
-> Show (Inference f)
forall f. Show f => Int -> Inference f -> ShowS
forall f. Show f => [Inference f] -> ShowS
forall f. Show f => Inference f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Inference f] -> ShowS
$cshowList :: forall f. Show f => [Inference f] -> ShowS
show :: Inference f -> String
$cshow :: forall f. Show f => Inference f -> String
showsPrec :: Int -> Inference f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> Inference f -> ShowS
Show, Inference f -> Inference f -> Bool
(Inference f -> Inference f -> Bool)
-> (Inference f -> Inference f -> Bool) -> Eq (Inference f)
forall f. Eq f => Inference f -> Inference f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Inference f -> Inference f -> Bool
$c/= :: forall f. Eq f => Inference f -> Inference f -> Bool
== :: Inference f -> Inference f -> Bool
$c== :: forall f. Eq f => Inference f -> Inference f -> Bool
Eq, Eq (Inference f)
Eq (Inference f)
-> (Inference f -> Inference f -> Ordering)
-> (Inference f -> Inference f -> Bool)
-> (Inference f -> Inference f -> Bool)
-> (Inference f -> Inference f -> Bool)
-> (Inference f -> Inference f -> Bool)
-> (Inference f -> Inference f -> Inference f)
-> (Inference f -> Inference f -> Inference f)
-> Ord (Inference f)
Inference f -> Inference f -> Bool
Inference f -> Inference f -> Ordering
Inference f -> Inference f -> Inference f
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f. Ord f => Eq (Inference f)
forall f. Ord f => Inference f -> Inference f -> Bool
forall f. Ord f => Inference f -> Inference f -> Ordering
forall f. Ord f => Inference f -> Inference f -> Inference f
min :: Inference f -> Inference f -> Inference f
$cmin :: forall f. Ord f => Inference f -> Inference f -> Inference f
max :: Inference f -> Inference f -> Inference f
$cmax :: forall f. Ord f => Inference f -> Inference f -> Inference f
>= :: Inference f -> Inference f -> Bool
$c>= :: forall f. Ord f => Inference f -> Inference f -> Bool
> :: Inference f -> Inference f -> Bool
$c> :: forall f. Ord f => Inference f -> Inference f -> Bool
<= :: Inference f -> Inference f -> Bool
$c<= :: forall f. Ord f => Inference f -> Inference f -> Bool
< :: Inference f -> Inference f -> Bool
$c< :: forall f. Ord f => Inference f -> Inference f -> Bool
compare :: Inference f -> Inference f -> Ordering
$ccompare :: forall f. Ord f => Inference f -> Inference f -> Ordering
$cp1Ord :: forall f. Ord f => Eq (Inference f)
Ord, a -> Inference b -> Inference a
(a -> b) -> Inference a -> Inference b
(forall a b. (a -> b) -> Inference a -> Inference b)
-> (forall a b. a -> Inference b -> Inference a)
-> Functor Inference
forall a b. a -> Inference b -> Inference a
forall a b. (a -> b) -> Inference a -> Inference b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Inference b -> Inference a
$c<$ :: forall a b. a -> Inference b -> Inference a
fmap :: (a -> b) -> Inference a -> Inference b
$cfmap :: forall a b. (a -> b) -> Inference a -> Inference b
Functor, Inference a -> Bool
(a -> m) -> Inference a -> m
(a -> b -> b) -> b -> Inference a -> b
(forall m. Monoid m => Inference m -> m)
-> (forall m a. Monoid m => (a -> m) -> Inference a -> m)
-> (forall m a. Monoid m => (a -> m) -> Inference a -> m)
-> (forall a b. (a -> b -> b) -> b -> Inference a -> b)
-> (forall a b. (a -> b -> b) -> b -> Inference a -> b)
-> (forall b a. (b -> a -> b) -> b -> Inference a -> b)
-> (forall b a. (b -> a -> b) -> b -> Inference a -> b)
-> (forall a. (a -> a -> a) -> Inference a -> a)
-> (forall a. (a -> a -> a) -> Inference a -> a)
-> (forall a. Inference a -> [a])
-> (forall a. Inference a -> Bool)
-> (forall a. Inference a -> Int)
-> (forall a. Eq a => a -> Inference a -> Bool)
-> (forall a. Ord a => Inference a -> a)
-> (forall a. Ord a => Inference a -> a)
-> (forall a. Num a => Inference a -> a)
-> (forall a. Num a => Inference a -> a)
-> Foldable Inference
forall a. Eq a => a -> Inference a -> Bool
forall a. Num a => Inference a -> a
forall a. Ord a => Inference a -> a
forall m. Monoid m => Inference m -> m
forall a. Inference a -> Bool
forall a. Inference a -> Int
forall a. Inference a -> [a]
forall a. (a -> a -> a) -> Inference a -> a
forall m a. Monoid m => (a -> m) -> Inference a -> m
forall b a. (b -> a -> b) -> b -> Inference a -> b
forall a b. (a -> b -> b) -> b -> Inference a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Inference a -> a
$cproduct :: forall a. Num a => Inference a -> a
sum :: Inference a -> a
$csum :: forall a. Num a => Inference a -> a
minimum :: Inference a -> a
$cminimum :: forall a. Ord a => Inference a -> a
maximum :: Inference a -> a
$cmaximum :: forall a. Ord a => Inference a -> a
elem :: a -> Inference a -> Bool
$celem :: forall a. Eq a => a -> Inference a -> Bool
length :: Inference a -> Int
$clength :: forall a. Inference a -> Int
null :: Inference a -> Bool
$cnull :: forall a. Inference a -> Bool
toList :: Inference a -> [a]
$ctoList :: forall a. Inference a -> [a]
foldl1 :: (a -> a -> a) -> Inference a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Inference a -> a
foldr1 :: (a -> a -> a) -> Inference a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Inference a -> a
foldl' :: (b -> a -> b) -> b -> Inference a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Inference a -> b
foldl :: (b -> a -> b) -> b -> Inference a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Inference a -> b
foldr' :: (a -> b -> b) -> b -> Inference a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Inference a -> b
foldr :: (a -> b -> b) -> b -> Inference a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Inference a -> b
foldMap' :: (a -> m) -> Inference a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Inference a -> m
foldMap :: (a -> m) -> Inference a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Inference a -> m
fold :: Inference m -> m
$cfold :: forall m. Monoid m => Inference m -> m
Foldable, Functor Inference
Foldable Inference
Functor Inference
-> Foldable Inference
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Inference a -> f (Inference b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Inference (f a) -> f (Inference a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Inference a -> m (Inference b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Inference (m a) -> m (Inference a))
-> Traversable Inference
(a -> f b) -> Inference a -> f (Inference b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Inference (m a) -> m (Inference a)
forall (f :: * -> *) a.
Applicative f =>
Inference (f a) -> f (Inference a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Inference a -> m (Inference b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inference a -> f (Inference b)
sequence :: Inference (m a) -> m (Inference a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Inference (m a) -> m (Inference a)
mapM :: (a -> m b) -> Inference a -> m (Inference b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Inference a -> m (Inference b)
sequenceA :: Inference (f a) -> f (Inference a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Inference (f a) -> f (Inference a)
traverse :: (a -> f b) -> Inference a -> f (Inference b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Inference a -> f (Inference b)
$cp2Traversable :: Foldable Inference
$cp1Traversable :: Functor Inference
Traversable)

-- | The antecedents of an inference.
antecedents :: Inference f -> [f]
antecedents :: Inference f -> [f]
antecedents = Inference f -> [f]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

-- | Contradiction is a special case of an inference that has the logical falsum
-- as the consequent.
newtype Contradiction f = Contradiction (Rule f)
  deriving (Int -> Contradiction f -> ShowS
[Contradiction f] -> ShowS
Contradiction f -> String
(Int -> Contradiction f -> ShowS)
-> (Contradiction f -> String)
-> ([Contradiction f] -> ShowS)
-> Show (Contradiction f)
forall f. Show f => Int -> Contradiction f -> ShowS
forall f. Show f => [Contradiction f] -> ShowS
forall f. Show f => Contradiction f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Contradiction f] -> ShowS
$cshowList :: forall f. Show f => [Contradiction f] -> ShowS
show :: Contradiction f -> String
$cshow :: forall f. Show f => Contradiction f -> String
showsPrec :: Int -> Contradiction f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> Contradiction f -> ShowS
Show, Contradiction f -> Contradiction f -> Bool
(Contradiction f -> Contradiction f -> Bool)
-> (Contradiction f -> Contradiction f -> Bool)
-> Eq (Contradiction f)
forall f. Eq f => Contradiction f -> Contradiction f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Contradiction f -> Contradiction f -> Bool
$c/= :: forall f. Eq f => Contradiction f -> Contradiction f -> Bool
== :: Contradiction f -> Contradiction f -> Bool
$c== :: forall f. Eq f => Contradiction f -> Contradiction f -> Bool
Eq, Eq (Contradiction f)
Eq (Contradiction f)
-> (Contradiction f -> Contradiction f -> Ordering)
-> (Contradiction f -> Contradiction f -> Bool)
-> (Contradiction f -> Contradiction f -> Bool)
-> (Contradiction f -> Contradiction f -> Bool)
-> (Contradiction f -> Contradiction f -> Bool)
-> (Contradiction f -> Contradiction f -> Contradiction f)
-> (Contradiction f -> Contradiction f -> Contradiction f)
-> Ord (Contradiction f)
Contradiction f -> Contradiction f -> Bool
Contradiction f -> Contradiction f -> Ordering
Contradiction f -> Contradiction f -> Contradiction f
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f. Ord f => Eq (Contradiction f)
forall f. Ord f => Contradiction f -> Contradiction f -> Bool
forall f. Ord f => Contradiction f -> Contradiction f -> Ordering
forall f.
Ord f =>
Contradiction f -> Contradiction f -> Contradiction f
min :: Contradiction f -> Contradiction f -> Contradiction f
$cmin :: forall f.
Ord f =>
Contradiction f -> Contradiction f -> Contradiction f
max :: Contradiction f -> Contradiction f -> Contradiction f
$cmax :: forall f.
Ord f =>
Contradiction f -> Contradiction f -> Contradiction f
>= :: Contradiction f -> Contradiction f -> Bool
$c>= :: forall f. Ord f => Contradiction f -> Contradiction f -> Bool
> :: Contradiction f -> Contradiction f -> Bool
$c> :: forall f. Ord f => Contradiction f -> Contradiction f -> Bool
<= :: Contradiction f -> Contradiction f -> Bool
$c<= :: forall f. Ord f => Contradiction f -> Contradiction f -> Bool
< :: Contradiction f -> Contradiction f -> Bool
$c< :: forall f. Ord f => Contradiction f -> Contradiction f -> Bool
compare :: Contradiction f -> Contradiction f -> Ordering
$ccompare :: forall f. Ord f => Contradiction f -> Contradiction f -> Ordering
$cp1Ord :: forall f. Ord f => Eq (Contradiction f)
Ord, a -> Contradiction b -> Contradiction a
(a -> b) -> Contradiction a -> Contradiction b
(forall a b. (a -> b) -> Contradiction a -> Contradiction b)
-> (forall a b. a -> Contradiction b -> Contradiction a)
-> Functor Contradiction
forall a b. a -> Contradiction b -> Contradiction a
forall a b. (a -> b) -> Contradiction a -> Contradiction b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Contradiction b -> Contradiction a
$c<$ :: forall a b. a -> Contradiction b -> Contradiction a
fmap :: (a -> b) -> Contradiction a -> Contradiction b
$cfmap :: forall a b. (a -> b) -> Contradiction a -> Contradiction b
Functor, a -> Contradiction a -> Bool
Contradiction m -> m
Contradiction a -> [a]
Contradiction a -> Bool
Contradiction a -> Int
Contradiction a -> a
Contradiction a -> a
Contradiction a -> a
Contradiction a -> a
(a -> m) -> Contradiction a -> m
(a -> m) -> Contradiction a -> m
(a -> b -> b) -> b -> Contradiction a -> b
(a -> b -> b) -> b -> Contradiction a -> b
(b -> a -> b) -> b -> Contradiction a -> b
(b -> a -> b) -> b -> Contradiction a -> b
(a -> a -> a) -> Contradiction a -> a
(a -> a -> a) -> Contradiction a -> a
(forall m. Monoid m => Contradiction m -> m)
-> (forall m a. Monoid m => (a -> m) -> Contradiction a -> m)
-> (forall m a. Monoid m => (a -> m) -> Contradiction a -> m)
-> (forall a b. (a -> b -> b) -> b -> Contradiction a -> b)
-> (forall a b. (a -> b -> b) -> b -> Contradiction a -> b)
-> (forall b a. (b -> a -> b) -> b -> Contradiction a -> b)
-> (forall b a. (b -> a -> b) -> b -> Contradiction a -> b)
-> (forall a. (a -> a -> a) -> Contradiction a -> a)
-> (forall a. (a -> a -> a) -> Contradiction a -> a)
-> (forall a. Contradiction a -> [a])
-> (forall a. Contradiction a -> Bool)
-> (forall a. Contradiction a -> Int)
-> (forall a. Eq a => a -> Contradiction a -> Bool)
-> (forall a. Ord a => Contradiction a -> a)
-> (forall a. Ord a => Contradiction a -> a)
-> (forall a. Num a => Contradiction a -> a)
-> (forall a. Num a => Contradiction a -> a)
-> Foldable Contradiction
forall a. Eq a => a -> Contradiction a -> Bool
forall a. Num a => Contradiction a -> a
forall a. Ord a => Contradiction a -> a
forall m. Monoid m => Contradiction m -> m
forall a. Contradiction a -> Bool
forall a. Contradiction a -> Int
forall a. Contradiction a -> [a]
forall a. (a -> a -> a) -> Contradiction a -> a
forall m a. Monoid m => (a -> m) -> Contradiction a -> m
forall b a. (b -> a -> b) -> b -> Contradiction a -> b
forall a b. (a -> b -> b) -> b -> Contradiction a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Contradiction a -> a
$cproduct :: forall a. Num a => Contradiction a -> a
sum :: Contradiction a -> a
$csum :: forall a. Num a => Contradiction a -> a
minimum :: Contradiction a -> a
$cminimum :: forall a. Ord a => Contradiction a -> a
maximum :: Contradiction a -> a
$cmaximum :: forall a. Ord a => Contradiction a -> a
elem :: a -> Contradiction a -> Bool
$celem :: forall a. Eq a => a -> Contradiction a -> Bool
length :: Contradiction a -> Int
$clength :: forall a. Contradiction a -> Int
null :: Contradiction a -> Bool
$cnull :: forall a. Contradiction a -> Bool
toList :: Contradiction a -> [a]
$ctoList :: forall a. Contradiction a -> [a]
foldl1 :: (a -> a -> a) -> Contradiction a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Contradiction a -> a
foldr1 :: (a -> a -> a) -> Contradiction a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Contradiction a -> a
foldl' :: (b -> a -> b) -> b -> Contradiction a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Contradiction a -> b
foldl :: (b -> a -> b) -> b -> Contradiction a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Contradiction a -> b
foldr' :: (a -> b -> b) -> b -> Contradiction a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Contradiction a -> b
foldr :: (a -> b -> b) -> b -> Contradiction a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Contradiction a -> b
foldMap' :: (a -> m) -> Contradiction a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Contradiction a -> m
foldMap :: (a -> m) -> Contradiction a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Contradiction a -> m
fold :: Contradiction m -> m
$cfold :: forall m. Monoid m => Contradiction m -> m
Foldable, Functor Contradiction
Foldable Contradiction
Functor Contradiction
-> Foldable Contradiction
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Contradiction a -> f (Contradiction b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Contradiction (f a) -> f (Contradiction a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Contradiction a -> m (Contradiction b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Contradiction (m a) -> m (Contradiction a))
-> Traversable Contradiction
(a -> f b) -> Contradiction a -> f (Contradiction b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Contradiction (m a) -> m (Contradiction a)
forall (f :: * -> *) a.
Applicative f =>
Contradiction (f a) -> f (Contradiction a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Contradiction a -> m (Contradiction b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Contradiction a -> f (Contradiction b)
sequence :: Contradiction (m a) -> m (Contradiction a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Contradiction (m a) -> m (Contradiction a)
mapM :: (a -> m b) -> Contradiction a -> m (Contradiction b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Contradiction a -> m (Contradiction b)
sequenceA :: Contradiction (f a) -> f (Contradiction a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Contradiction (f a) -> f (Contradiction a)
traverse :: (a -> f b) -> Contradiction a -> f (Contradiction b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Contradiction a -> f (Contradiction b)
$cp2Traversable :: Foldable Contradiction
$cp1Traversable :: Functor Contradiction
Traversable)

-- | A sequent is a logical inference, annotated with a label.
-- Linked sequents form derivations.
data Sequent f = Sequent f (Inference f)
  deriving (Int -> Sequent f -> ShowS
[Sequent f] -> ShowS
Sequent f -> String
(Int -> Sequent f -> ShowS)
-> (Sequent f -> String)
-> ([Sequent f] -> ShowS)
-> Show (Sequent f)
forall f. Show f => Int -> Sequent f -> ShowS
forall f. Show f => [Sequent f] -> ShowS
forall f. Show f => Sequent f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sequent f] -> ShowS
$cshowList :: forall f. Show f => [Sequent f] -> ShowS
show :: Sequent f -> String
$cshow :: forall f. Show f => Sequent f -> String
showsPrec :: Int -> Sequent f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> Sequent f -> ShowS
Show, Sequent f -> Sequent f -> Bool
(Sequent f -> Sequent f -> Bool)
-> (Sequent f -> Sequent f -> Bool) -> Eq (Sequent f)
forall f. Eq f => Sequent f -> Sequent f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sequent f -> Sequent f -> Bool
$c/= :: forall f. Eq f => Sequent f -> Sequent f -> Bool
== :: Sequent f -> Sequent f -> Bool
$c== :: forall f. Eq f => Sequent f -> Sequent f -> Bool
Eq, Eq (Sequent f)
Eq (Sequent f)
-> (Sequent f -> Sequent f -> Ordering)
-> (Sequent f -> Sequent f -> Bool)
-> (Sequent f -> Sequent f -> Bool)
-> (Sequent f -> Sequent f -> Bool)
-> (Sequent f -> Sequent f -> Bool)
-> (Sequent f -> Sequent f -> Sequent f)
-> (Sequent f -> Sequent f -> Sequent f)
-> Ord (Sequent f)
Sequent f -> Sequent f -> Bool
Sequent f -> Sequent f -> Ordering
Sequent f -> Sequent f -> Sequent f
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f. Ord f => Eq (Sequent f)
forall f. Ord f => Sequent f -> Sequent f -> Bool
forall f. Ord f => Sequent f -> Sequent f -> Ordering
forall f. Ord f => Sequent f -> Sequent f -> Sequent f
min :: Sequent f -> Sequent f -> Sequent f
$cmin :: forall f. Ord f => Sequent f -> Sequent f -> Sequent f
max :: Sequent f -> Sequent f -> Sequent f
$cmax :: forall f. Ord f => Sequent f -> Sequent f -> Sequent f
>= :: Sequent f -> Sequent f -> Bool
$c>= :: forall f. Ord f => Sequent f -> Sequent f -> Bool
> :: Sequent f -> Sequent f -> Bool
$c> :: forall f. Ord f => Sequent f -> Sequent f -> Bool
<= :: Sequent f -> Sequent f -> Bool
$c<= :: forall f. Ord f => Sequent f -> Sequent f -> Bool
< :: Sequent f -> Sequent f -> Bool
$c< :: forall f. Ord f => Sequent f -> Sequent f -> Bool
compare :: Sequent f -> Sequent f -> Ordering
$ccompare :: forall f. Ord f => Sequent f -> Sequent f -> Ordering
$cp1Ord :: forall f. Ord f => Eq (Sequent f)
Ord, a -> Sequent b -> Sequent a
(a -> b) -> Sequent a -> Sequent b
(forall a b. (a -> b) -> Sequent a -> Sequent b)
-> (forall a b. a -> Sequent b -> Sequent a) -> Functor Sequent
forall a b. a -> Sequent b -> Sequent a
forall a b. (a -> b) -> Sequent a -> Sequent b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Sequent b -> Sequent a
$c<$ :: forall a b. a -> Sequent b -> Sequent a
fmap :: (a -> b) -> Sequent a -> Sequent b
$cfmap :: forall a b. (a -> b) -> Sequent a -> Sequent b
Functor, Sequent a -> Bool
(a -> m) -> Sequent a -> m
(a -> b -> b) -> b -> Sequent a -> b
(forall m. Monoid m => Sequent m -> m)
-> (forall m a. Monoid m => (a -> m) -> Sequent a -> m)
-> (forall m a. Monoid m => (a -> m) -> Sequent a -> m)
-> (forall a b. (a -> b -> b) -> b -> Sequent a -> b)
-> (forall a b. (a -> b -> b) -> b -> Sequent a -> b)
-> (forall b a. (b -> a -> b) -> b -> Sequent a -> b)
-> (forall b a. (b -> a -> b) -> b -> Sequent a -> b)
-> (forall a. (a -> a -> a) -> Sequent a -> a)
-> (forall a. (a -> a -> a) -> Sequent a -> a)
-> (forall a. Sequent a -> [a])
-> (forall a. Sequent a -> Bool)
-> (forall a. Sequent a -> Int)
-> (forall a. Eq a => a -> Sequent a -> Bool)
-> (forall a. Ord a => Sequent a -> a)
-> (forall a. Ord a => Sequent a -> a)
-> (forall a. Num a => Sequent a -> a)
-> (forall a. Num a => Sequent a -> a)
-> Foldable Sequent
forall a. Eq a => a -> Sequent a -> Bool
forall a. Num a => Sequent a -> a
forall a. Ord a => Sequent a -> a
forall m. Monoid m => Sequent m -> m
forall a. Sequent a -> Bool
forall a. Sequent a -> Int
forall a. Sequent a -> [a]
forall a. (a -> a -> a) -> Sequent a -> a
forall m a. Monoid m => (a -> m) -> Sequent a -> m
forall b a. (b -> a -> b) -> b -> Sequent a -> b
forall a b. (a -> b -> b) -> b -> Sequent a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Sequent a -> a
$cproduct :: forall a. Num a => Sequent a -> a
sum :: Sequent a -> a
$csum :: forall a. Num a => Sequent a -> a
minimum :: Sequent a -> a
$cminimum :: forall a. Ord a => Sequent a -> a
maximum :: Sequent a -> a
$cmaximum :: forall a. Ord a => Sequent a -> a
elem :: a -> Sequent a -> Bool
$celem :: forall a. Eq a => a -> Sequent a -> Bool
length :: Sequent a -> Int
$clength :: forall a. Sequent a -> Int
null :: Sequent a -> Bool
$cnull :: forall a. Sequent a -> Bool
toList :: Sequent a -> [a]
$ctoList :: forall a. Sequent a -> [a]
foldl1 :: (a -> a -> a) -> Sequent a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Sequent a -> a
foldr1 :: (a -> a -> a) -> Sequent a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Sequent a -> a
foldl' :: (b -> a -> b) -> b -> Sequent a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Sequent a -> b
foldl :: (b -> a -> b) -> b -> Sequent a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Sequent a -> b
foldr' :: (a -> b -> b) -> b -> Sequent a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Sequent a -> b
foldr :: (a -> b -> b) -> b -> Sequent a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Sequent a -> b
foldMap' :: (a -> m) -> Sequent a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Sequent a -> m
foldMap :: (a -> m) -> Sequent a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Sequent a -> m
fold :: Sequent m -> m
$cfold :: forall m. Monoid m => Sequent m -> m
Foldable, Functor Sequent
Foldable Sequent
Functor Sequent
-> Foldable Sequent
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Sequent a -> f (Sequent b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Sequent (f a) -> f (Sequent a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Sequent a -> m (Sequent b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Sequent (m a) -> m (Sequent a))
-> Traversable Sequent
(a -> f b) -> Sequent a -> f (Sequent b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Sequent (m a) -> m (Sequent a)
forall (f :: * -> *) a.
Applicative f =>
Sequent (f a) -> f (Sequent a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sequent a -> m (Sequent b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Sequent a -> f (Sequent b)
sequence :: Sequent (m a) -> m (Sequent a)
$csequence :: forall (m :: * -> *) a. Monad m => Sequent (m a) -> m (Sequent a)
mapM :: (a -> m b) -> Sequent a -> m (Sequent b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sequent a -> m (Sequent b)
sequenceA :: Sequent (f a) -> f (Sequent a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Sequent (f a) -> f (Sequent a)
traverse :: (a -> f b) -> Sequent a -> f (Sequent b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Sequent a -> f (Sequent b)
$cp2Traversable :: Foldable Sequent
$cp1Traversable :: Functor Sequent
Traversable)

sequentMap :: Ord f => [Sequent f] -> Map f (Inference f)
sequentMap :: [Sequent f] -> Map f (Inference f)
sequentMap [Sequent f]
ss = [(f, Inference f)] -> Map f (Inference f)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(f
f, Inference f
e) | Sequent f
f Inference f
e <- [Sequent f]
ss]

-- | Construct a mapping between inference labels and their correspondent
-- formulas.
labeling :: Ord f => [Sequent f] -> Map f LogicalExpression
labeling :: [Sequent f] -> Map f LogicalExpression
labeling = (Inference f -> LogicalExpression)
-> Map f (Inference f) -> Map f LogicalExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Inference f -> LogicalExpression
forall f. Inference f -> LogicalExpression
consequent (Map f (Inference f) -> Map f LogicalExpression)
-> ([Sequent f] -> Map f (Inference f))
-> [Sequent f]
-> Map f LogicalExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sequent f] -> Map f (Inference f)
forall f. Ord f => [Sequent f] -> Map f (Inference f)
sequentMap

-- | A derivation is a directed asyclic graph of logical inferences.
-- In this graph nodes are formulas and edges are inference rules.
-- The type parameter @f@ is used to label and index the nodes.
newtype Derivation f = Derivation (Map f (Inference f))
  deriving (Int -> Derivation f -> ShowS
[Derivation f] -> ShowS
Derivation f -> String
(Int -> Derivation f -> ShowS)
-> (Derivation f -> String)
-> ([Derivation f] -> ShowS)
-> Show (Derivation f)
forall f. Show f => Int -> Derivation f -> ShowS
forall f. Show f => [Derivation f] -> ShowS
forall f. Show f => Derivation f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Derivation f] -> ShowS
$cshowList :: forall f. Show f => [Derivation f] -> ShowS
show :: Derivation f -> String
$cshow :: forall f. Show f => Derivation f -> String
showsPrec :: Int -> Derivation f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> Derivation f -> ShowS
Show, Derivation f -> Derivation f -> Bool
(Derivation f -> Derivation f -> Bool)
-> (Derivation f -> Derivation f -> Bool) -> Eq (Derivation f)
forall f. Eq f => Derivation f -> Derivation f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Derivation f -> Derivation f -> Bool
$c/= :: forall f. Eq f => Derivation f -> Derivation f -> Bool
== :: Derivation f -> Derivation f -> Bool
$c== :: forall f. Eq f => Derivation f -> Derivation f -> Bool
Eq, Eq (Derivation f)
Eq (Derivation f)
-> (Derivation f -> Derivation f -> Ordering)
-> (Derivation f -> Derivation f -> Bool)
-> (Derivation f -> Derivation f -> Bool)
-> (Derivation f -> Derivation f -> Bool)
-> (Derivation f -> Derivation f -> Bool)
-> (Derivation f -> Derivation f -> Derivation f)
-> (Derivation f -> Derivation f -> Derivation f)
-> Ord (Derivation f)
Derivation f -> Derivation f -> Bool
Derivation f -> Derivation f -> Ordering
Derivation f -> Derivation f -> Derivation f
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f. Ord f => Eq (Derivation f)
forall f. Ord f => Derivation f -> Derivation f -> Bool
forall f. Ord f => Derivation f -> Derivation f -> Ordering
forall f. Ord f => Derivation f -> Derivation f -> Derivation f
min :: Derivation f -> Derivation f -> Derivation f
$cmin :: forall f. Ord f => Derivation f -> Derivation f -> Derivation f
max :: Derivation f -> Derivation f -> Derivation f
$cmax :: forall f. Ord f => Derivation f -> Derivation f -> Derivation f
>= :: Derivation f -> Derivation f -> Bool
$c>= :: forall f. Ord f => Derivation f -> Derivation f -> Bool
> :: Derivation f -> Derivation f -> Bool
$c> :: forall f. Ord f => Derivation f -> Derivation f -> Bool
<= :: Derivation f -> Derivation f -> Bool
$c<= :: forall f. Ord f => Derivation f -> Derivation f -> Bool
< :: Derivation f -> Derivation f -> Bool
$c< :: forall f. Ord f => Derivation f -> Derivation f -> Bool
compare :: Derivation f -> Derivation f -> Ordering
$ccompare :: forall f. Ord f => Derivation f -> Derivation f -> Ordering
$cp1Ord :: forall f. Ord f => Eq (Derivation f)
Ord, b -> Derivation f -> Derivation f
NonEmpty (Derivation f) -> Derivation f
Derivation f -> Derivation f -> Derivation f
(Derivation f -> Derivation f -> Derivation f)
-> (NonEmpty (Derivation f) -> Derivation f)
-> (forall b. Integral b => b -> Derivation f -> Derivation f)
-> Semigroup (Derivation f)
forall b. Integral b => b -> Derivation f -> Derivation f
forall f. Ord f => NonEmpty (Derivation f) -> Derivation f
forall f. Ord f => Derivation f -> Derivation f -> Derivation f
forall f b.
(Ord f, Integral b) =>
b -> Derivation f -> Derivation f
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> Derivation f -> Derivation f
$cstimes :: forall f b.
(Ord f, Integral b) =>
b -> Derivation f -> Derivation f
sconcat :: NonEmpty (Derivation f) -> Derivation f
$csconcat :: forall f. Ord f => NonEmpty (Derivation f) -> Derivation f
<> :: Derivation f -> Derivation f -> Derivation f
$c<> :: forall f. Ord f => Derivation f -> Derivation f -> Derivation f
Semigroup, Semigroup (Derivation f)
Derivation f
Semigroup (Derivation f)
-> Derivation f
-> (Derivation f -> Derivation f -> Derivation f)
-> ([Derivation f] -> Derivation f)
-> Monoid (Derivation f)
[Derivation f] -> Derivation f
Derivation f -> Derivation f -> Derivation f
forall f. Ord f => Semigroup (Derivation f)
forall f. Ord f => Derivation f
forall f. Ord f => [Derivation f] -> Derivation f
forall f. Ord f => Derivation f -> Derivation f -> Derivation f
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Derivation f] -> Derivation f
$cmconcat :: forall f. Ord f => [Derivation f] -> Derivation f
mappend :: Derivation f -> Derivation f -> Derivation f
$cmappend :: forall f. Ord f => Derivation f -> Derivation f -> Derivation f
mempty :: Derivation f
$cmempty :: forall f. Ord f => Derivation f
$cp1Monoid :: forall f. Ord f => Semigroup (Derivation f)
Monoid)

-- | Attach a sequent to a derivation.
addSequent :: Ord f => Derivation f -> Sequent f -> Derivation f
addSequent :: Derivation f -> Sequent f -> Derivation f
addSequent (Derivation Map f (Inference f)
m) (Sequent f
f Inference f
i) = Map f (Inference f) -> Derivation f
forall f. Map f (Inference f) -> Derivation f
Derivation (f -> Inference f -> Map f (Inference f) -> Map f (Inference f)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert f
f Inference f
i Map f (Inference f)
m)

fromDerivation :: Derivation f -> [Sequent f]
fromDerivation :: Derivation f -> [Sequent f]
fromDerivation (Derivation Map f (Inference f)
m) = ((f, Inference f) -> Sequent f)
-> [(f, Inference f)] -> [Sequent f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f -> Inference f -> Sequent f) -> (f, Inference f) -> Sequent f
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry f -> Inference f -> Sequent f
forall f. f -> Inference f -> Sequent f
Sequent) (Map f (Inference f) -> [(f, Inference f)]
forall k a. Map k a -> [(k, a)]
M.toList Map f (Inference f)
m)

-- | Traverse the given derivation breadth-first and produce a list of sequents.
breadthFirst :: Ord f => Derivation f -> [Sequent f]
breadthFirst :: Derivation f -> [Sequent f]
breadthFirst Derivation f
d = (Sequent f -> Sequent f -> Ordering) -> [Sequent f] -> [Sequent f]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Integer, Rule f, LogicalExpression)
-> (Integer, Rule f, LogicalExpression) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((Integer, Rule f, LogicalExpression)
 -> (Integer, Rule f, LogicalExpression) -> Ordering)
-> (Sequent f -> (Integer, Rule f, LogicalExpression))
-> Sequent f
-> Sequent f
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Sequent f -> (Integer, Rule f, LogicalExpression)
criteria) (Derivation f -> [Sequent f]
forall f. Derivation f -> [Sequent f]
fromDerivation Derivation f
d)
  where criteria :: Sequent f -> (Integer, Rule f, LogicalExpression)
criteria (Sequent f
l (Inference Rule f
r LogicalExpression
f)) = (Derivation f -> Map f Integer
forall f. Ord f => Derivation f -> Map f Integer
distances Derivation f
d Map f Integer -> f -> Integer
forall k a. Ord k => Map k a -> k -> a
! f
l, Rule f
r, LogicalExpression
f)

distances :: Ord f => Derivation f -> Map f Integer
distances :: Derivation f -> Map f Integer
distances (Derivation Map f (Inference f)
m) = (Inference f -> Integer) -> Map f (Inference f) -> Map f Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Inference f -> Integer
forall p. (Num p, Ord p) => Inference f -> p
distance Map f (Inference f)
m
  where
    distance :: Inference f -> p
distance Inference f
i
      | [f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Inference f -> [f]
forall a. Inference a -> [a]
antecedents Inference f
i) = p
0
      | Bool
otherwise = p
1 p -> p -> p
forall a. Num a => a -> a -> a
+ [p] -> p
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((f -> p) -> [f] -> [p]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\f
a -> Inference f -> p
distance (Map f (Inference f)
m Map f (Inference f) -> f -> Inference f
forall k a. Ord k => Map k a -> k -> a
! f
a)) (Inference f -> [f]
forall a. Inference a -> [a]
antecedents Inference f
i))

-- | A refutation is a special case of a derivation that results in a
-- contradiction. A successful proof produces by an automated theorem prover
-- is a proof by refutation.
data Refutation f = Refutation (Derivation f) (Contradiction f)
  deriving (Int -> Refutation f -> ShowS
[Refutation f] -> ShowS
Refutation f -> String
(Int -> Refutation f -> ShowS)
-> (Refutation f -> String)
-> ([Refutation f] -> ShowS)
-> Show (Refutation f)
forall f. Show f => Int -> Refutation f -> ShowS
forall f. Show f => [Refutation f] -> ShowS
forall f. Show f => Refutation f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Refutation f] -> ShowS
$cshowList :: forall f. Show f => [Refutation f] -> ShowS
show :: Refutation f -> String
$cshow :: forall f. Show f => Refutation f -> String
showsPrec :: Int -> Refutation f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> Refutation f -> ShowS
Show, Refutation f -> Refutation f -> Bool
(Refutation f -> Refutation f -> Bool)
-> (Refutation f -> Refutation f -> Bool) -> Eq (Refutation f)
forall f. Eq f => Refutation f -> Refutation f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Refutation f -> Refutation f -> Bool
$c/= :: forall f. Eq f => Refutation f -> Refutation f -> Bool
== :: Refutation f -> Refutation f -> Bool
$c== :: forall f. Eq f => Refutation f -> Refutation f -> Bool
Eq, Eq (Refutation f)
Eq (Refutation f)
-> (Refutation f -> Refutation f -> Ordering)
-> (Refutation f -> Refutation f -> Bool)
-> (Refutation f -> Refutation f -> Bool)
-> (Refutation f -> Refutation f -> Bool)
-> (Refutation f -> Refutation f -> Bool)
-> (Refutation f -> Refutation f -> Refutation f)
-> (Refutation f -> Refutation f -> Refutation f)
-> Ord (Refutation f)
Refutation f -> Refutation f -> Bool
Refutation f -> Refutation f -> Ordering
Refutation f -> Refutation f -> Refutation f
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f. Ord f => Eq (Refutation f)
forall f. Ord f => Refutation f -> Refutation f -> Bool
forall f. Ord f => Refutation f -> Refutation f -> Ordering
forall f. Ord f => Refutation f -> Refutation f -> Refutation f
min :: Refutation f -> Refutation f -> Refutation f
$cmin :: forall f. Ord f => Refutation f -> Refutation f -> Refutation f
max :: Refutation f -> Refutation f -> Refutation f
$cmax :: forall f. Ord f => Refutation f -> Refutation f -> Refutation f
>= :: Refutation f -> Refutation f -> Bool
$c>= :: forall f. Ord f => Refutation f -> Refutation f -> Bool
> :: Refutation f -> Refutation f -> Bool
$c> :: forall f. Ord f => Refutation f -> Refutation f -> Bool
<= :: Refutation f -> Refutation f -> Bool
$c<= :: forall f. Ord f => Refutation f -> Refutation f -> Bool
< :: Refutation f -> Refutation f -> Bool
$c< :: forall f. Ord f => Refutation f -> Refutation f -> Bool
compare :: Refutation f -> Refutation f -> Ordering
$ccompare :: forall f. Ord f => Refutation f -> Refutation f -> Ordering
$cp1Ord :: forall f. Ord f => Eq (Refutation f)
Ord)

-- | The solution produced by an automated first-order theorem prover.
data Solution
  = Saturation (Derivation Integer)
  -- ^ A theorem can be disproven if the prover constructs a saturated set of
  -- first-order clauses.
  | Proof (Refutation Integer)
  -- ^ A theorem can be proven if the prover derives contradiction (the empty
  -- clause) from the set of axioms and the negated conjecture.
  deriving (Int -> Solution -> ShowS
[Solution] -> ShowS
Solution -> String
(Int -> Solution -> ShowS)
-> (Solution -> String) -> ([Solution] -> ShowS) -> Show Solution
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Solution] -> ShowS
$cshowList :: [Solution] -> ShowS
show :: Solution -> String
$cshow :: Solution -> String
showsPrec :: Int -> Solution -> ShowS
$cshowsPrec :: Int -> Solution -> ShowS
Show, Solution -> Solution -> Bool
(Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool) -> Eq Solution
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Solution -> Solution -> Bool
$c/= :: Solution -> Solution -> Bool
== :: Solution -> Solution -> Bool
$c== :: Solution -> Solution -> Bool
Eq, Eq Solution
Eq Solution
-> (Solution -> Solution -> Ordering)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Bool)
-> (Solution -> Solution -> Solution)
-> (Solution -> Solution -> Solution)
-> Ord Solution
Solution -> Solution -> Bool
Solution -> Solution -> Ordering
Solution -> Solution -> Solution
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Solution -> Solution -> Solution
$cmin :: Solution -> Solution -> Solution
max :: Solution -> Solution -> Solution
$cmax :: Solution -> Solution -> Solution
>= :: Solution -> Solution -> Bool
$c>= :: Solution -> Solution -> Bool
> :: Solution -> Solution -> Bool
$c> :: Solution -> Solution -> Bool
<= :: Solution -> Solution -> Bool
$c<= :: Solution -> Solution -> Bool
< :: Solution -> Solution -> Bool
$c< :: Solution -> Solution -> Bool
compare :: Solution -> Solution -> Ordering
$ccompare :: Solution -> Solution -> Ordering
$cp1Ord :: Eq Solution
Ord)