Data.Logic.ATP.Quantified

IsQuantified is a subclass of IsPropositional of formula types that support existential and universal quantification.

Documentation

data Quant

The two types of quantification

Constructors

(:!:)

for_all

(:?:)

exists

Instances

Eq Quant

Methods

(==) :: Quant -> Quant -> Bool

(/=) :: Quant -> Quant -> Bool

Data Quant

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quant -> c Quant

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quant

toConstr :: Quant -> Constr

dataTypeOf :: Quant -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Quant)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)

gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r

gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant

Ord Quant

Methods

compare :: Quant -> Quant -> Ordering

(<) :: Quant -> Quant -> Bool

(<=) :: Quant -> Quant -> Bool

(>) :: Quant -> Quant -> Bool

(>=) :: Quant -> Quant -> Bool

max :: Quant -> Quant -> Quant

min :: Quant -> Quant -> Quant

Show Quant

Methods

showsPrec :: Int -> Quant -> ShowS

show :: Quant -> String

showList :: [Quant] -> ShowS

class (IsPropositional formula, IsVariable (VarOf formula)) => IsQuantified formula where

Class of quantified formulas.

Minimal complete definition

quant, foldQuantified

Associated Types

type VarOf formula

Methods

quant :: Quant -> VarOf formula -> formula -> formula

foldQuantified :: (Quant -> VarOf formula -> formula -> r) -> (formula -> BinOp -> formula -> r) -> (formula -> r) -> (Bool -> r) -> (AtomOf formula -> r) -> formula -> r

Instances

(IsPropositional (QFormula v atom), IsVariable v, IsAtom atom) => IsQuantified (QFormula v atom)

Associated Types

type VarOf (QFormula v atom) :: *

Methods

quant :: Quant -> VarOf (QFormula v atom) -> QFormula v atom -> QFormula v atom

foldQuantified :: (Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r

for_all :: IsQuantified formula => VarOf formula -> formula -> formula

(∀) :: IsQuantified formula => VarOf formula -> formula -> formula infixr 1

∀ can't be a function when -XUnicodeSyntax is enabled.

exists :: IsQuantified formula => VarOf formula -> formula -> formula

(∃) :: IsQuantified formula => VarOf formula -> formula -> formula infixr 1

precedenceQuantified :: forall formula. IsQuantified formula => formula -> Precedence

associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity

prettyQuantified :: forall fof v. (IsQuantified fof, v ~ VarOf fof) => Side -> PrettyLevel -> Rational -> fof -> Doc

Implementation of Pretty for IsQuantified types.

showQuantified :: IsQuantified formula => Side -> Int -> formula -> ShowS

Implementation of showsPrec for IsQuantified types.

zipQuantified :: IsQuantified formula => (Quant -> VarOf formula -> formula -> Quant -> VarOf formula -> formula -> Maybe r) -> (formula -> BinOp -> formula -> formula -> BinOp -> formula -> Maybe r) -> (formula -> formula -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (AtomOf formula -> AtomOf formula -> Maybe r) -> formula -> formula -> Maybe r

Combine two formulas if they are similar.

convertQuantified :: forall f1 f2. (IsQuantified f1, IsQuantified f2) => (AtomOf f1 -> AtomOf f2) -> (VarOf f1 -> VarOf f2) -> f1 -> f2

Convert any instance of IsQuantified to any other by specifying the result type.

onatomsQuantified :: IsQuantified formula => (AtomOf formula -> AtomOf formula) -> formula -> formula

overatomsQuantified :: IsQuantified fof => (AtomOf fof -> r -> r) -> fof -> r -> r

Concrete instance of a quantified formula type

data QFormula v atom

Constructors

F

T

Atom atom

Not (QFormula v atom)

And (QFormula v atom) (QFormula v atom)

Or (QFormula v atom) (QFormula v atom)

Imp (QFormula v atom) (QFormula v atom)

Iff (QFormula v atom) (QFormula v atom)

Forall v (QFormula v atom)

Exists v (QFormula v atom)

Instances

IsFirstOrder EqFormula

IsFirstOrder ApFormula

IsFirstOrder Formula

(Eq v, Eq atom) => Eq (QFormula v atom)

Methods

(==) :: QFormula v atom -> QFormula v atom -> Bool

(/=) :: QFormula v atom -> QFormula v atom -> Bool

(Data v, Data atom) => Data (QFormula v atom)

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QFormula v atom -> c (QFormula v atom)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (QFormula v atom)

toConstr :: QFormula v atom -> Constr

dataTypeOf :: QFormula v atom -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (QFormula v atom))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (QFormula v atom))

gmapT :: (forall b. Data b => b -> b) -> QFormula v atom -> QFormula v atom

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QFormula v atom -> r

gmapQ :: (forall d. Data d => d -> u) -> QFormula v atom -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> QFormula v atom -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QFormula v atom -> m (QFormula v atom)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QFormula v atom -> m (QFormula v atom)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QFormula v atom -> m (QFormula v atom)

(Ord v, Ord atom) => Ord (QFormula v atom)

Methods

compare :: QFormula v atom -> QFormula v atom -> Ordering

(<) :: QFormula v atom -> QFormula v atom -> Bool

(<=) :: QFormula v atom -> QFormula v atom -> Bool

(>) :: QFormula v atom -> QFormula v atom -> Bool

(>=) :: QFormula v atom -> QFormula v atom -> Bool

max :: QFormula v atom -> QFormula v atom -> QFormula v atom

min :: QFormula v atom -> QFormula v atom -> QFormula v atom

(Read v, Read atom) => Read (QFormula v atom)

Methods

readsPrec :: Int -> ReadS (QFormula v atom)

readList :: ReadS [QFormula v atom]

readPrec :: ReadPrec (QFormula v atom)

readListPrec :: ReadPrec [QFormula v atom]

IsQuantified (QFormula v atom) => Show (QFormula v atom)

Methods

showsPrec :: Int -> QFormula v atom -> ShowS

show :: QFormula v atom -> String

showList :: [QFormula v atom] -> ShowS

(HasApply atom, IsTerm term, (~) * term (TermOf atom), (~) * v (TVarOf term)) => Pretty (QFormula v atom)

Methods

pPrintPrec :: PrettyLevel -> Rational -> QFormula v atom -> Doc

pPrint :: QFormula v atom -> Doc

pPrintList :: PrettyLevel -> [QFormula v atom] -> Doc

IsQuantified (QFormula v atom) => HasFixity (QFormula v atom)

Methods

precedence :: QFormula v atom -> Precedence

associativity :: QFormula v atom -> Associativity

(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsFormula (QFormula v atom)

Associated Types

type AtomOf (QFormula v atom) :: *

Methods

true :: QFormula v atom

false :: QFormula v atom

asBool :: QFormula v atom -> Maybe Bool

atomic :: AtomOf (QFormula v atom) -> QFormula v atom

overatoms :: (AtomOf (QFormula v atom) -> r -> r) -> QFormula v atom -> r -> r

onatoms :: (AtomOf (QFormula v atom) -> AtomOf (QFormula v atom)) -> QFormula v atom -> QFormula v atom

(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsLiteral (QFormula v atom)

Methods

naiveNegate :: QFormula v atom -> QFormula v atom

foldNegation :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> QFormula v atom -> r

foldLiteral' :: (QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r

(IsFormula (QFormula v atom), HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsPropositional (QFormula v atom)

Methods

(.|.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

(.&.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

(.<=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

(.=>.) :: QFormula v atom -> QFormula v atom -> QFormula v atom

foldPropositional' :: (QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r

foldCombination :: (QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> (QFormula v atom -> QFormula v atom -> r) -> QFormula v atom -> r

(IsPropositional (QFormula v atom), IsVariable v, IsAtom atom) => IsQuantified (QFormula v atom)

Associated Types

type VarOf (QFormula v atom) :: *

Methods

quant :: Quant -> VarOf (QFormula v atom) -> QFormula v atom -> QFormula v atom

foldQuantified :: (Quant -> VarOf (QFormula v atom) -> QFormula v atom -> r) -> (QFormula v atom -> BinOp -> QFormula v atom -> r) -> (QFormula v atom -> r) -> (Bool -> r) -> (AtomOf (QFormula v atom) -> r) -> QFormula v atom -> r

type AtomOf (QFormula v atom)

type AtomOf (QFormula v atom) = atom

type VarOf (QFormula v atom)

type VarOf (QFormula v atom) = v