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

Data Quant

Ord Quant

Show Quant

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

Class of quantified formulas.

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)

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)

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

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

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

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

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

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

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

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

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

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

type AtomOf (QFormula v atom) = atom

type VarOf (QFormula v atom) = v