





Synopsis 




Basic undecorated formulae and terms



Basic (undecorated) firstorder formulae



Basic (undecorated) terms



Equivalence
Don't let the type context of these wrapper function confuse you :)  the important special case is just:
(.<=>.) :: Formula > Formula > Formula 


Implication



Reverse implication



Disjunction/OR



Conjunction/AND



XOR



NOR



NAND



Negation



Equality



Inequality



Universal quantification



Existential quantification



Predicate symbol application



Variable



Function symbol application (constants are encoded as nullary functions)



Number literal



Doublequoted string literal, called Distinct Object in TPTP's grammar


General decorated formulae and terms


data Formula0 term formula  Source 

See http://haskell.org/haskellwiki/Indirect_composite for the point of the type parameters (they allow for future decorations, e.g. monadic subformulae). If you don't need decorations, you can just use Formula and the wrapped constructors above.
 Constructors  BinOp formula BinOp formula  Binary connective application
 InfixPred term InfixPred term  Infix predicate application (equalities, inequalities)
 PredApp AtomicWord [term]  Predicate application
 Quant Quant [V] formula  Quantified formula
 :~: formula  Negation

 Instances  



See http://haskell.org/haskellwiki/Indirect_composite for the point of the type parameters (they allow for future decorations). If you don't need decorations, you can just use Term and the wrapped constructors above.
 Constructors  Var V  Variable
 NumberLitTerm Double  Number literal
 DistinctObjectTerm String  Doublequoted item
 FunApp AtomicWord [term]  Function symbol application (constants are encoded as nullary functions)

 Instances  



Formulae whose subexpressions are wrapped in the given type constructor c.
For example:
 c = Identity: Plain formulae
 c = Maybe: Formulae that may contain "holes"
 c = IORef: (Mutable) formulae with mutable subexpressions
 Constructors   Instances  



Terms whose subterms are wrapped in the given type constructor c
 Constructors   Instances  



Binary formula connectives
 Constructors  :<=>:  Equivalence
 :=>:  Implication
 :<=:  Reverse Implication
 :&:  AND
 ::  OR
 :~&:  NAND
 :~:  NOR
 :<~>:  XOR

 Instances  



Term > Term > Formula infix connectives
 Constructors   Instances  



Quantifier specification
 Constructors   Instances  


Formula Metadata



A line of a TPTP file: Annotated formula, comment or include statement.
 Constructors   Instances  



Annotations about the formulas origin
 Constructors   Instances  



Misc annotations
 Constructors  NoUsefulInfo   UsefulInfo [GTerm]  
 Instances  



Formula roles
 Constructors   Instances  



Metadata (the general_data rule in TPTP's grammar)
 Constructors   Instances  



Metadata (the general_term rule in TPTP's grammar)
 Constructors   Instances  


Gathering free Variables



 Methods   Obtain the free variables from a formula or term

  Instances  



Universally quantify all free variables in the formula



TPTP constant symbol/predicate symbol/function symbol identifiers (they are output in single quotes unless they are lower_words).
Tip: Use the XOverloadedStrings compiler flag if you don't want to have to type AtomicWord to construct an AtomicWord
 Constructors   Instances  



Variable names
 Constructors   Instances  


Fixedpoint style decorated formulae and terms


class Pointed a b  b > a where  Source 

This class is used in several utility functions involving F and T.
Conceptually point should be of type a > m a, but we need the extra flexibility to make restricted monads like Set instances.
Note: We have instance (Monad m) => Pointed a (m a), but Haddock currently doesn't display this.
  Methods    Instances  


class Copointed a b  b > a where  Source 

This class is used in several utility functions involving F and T.
Conceptually copoint should be of type w a > a, but let's keep the extra flexibility.
  Methods    Instances  


Utility functions











:: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t)))   => F t > r  Handle negation
 > Quant > [V] > F t > r  Handle quantification
 > F t > BinOp > F t > r  Handle binary op
 > T t > InfixPred > T t > r  Handle equality/inequality
 > AtomicWord > [T t] > r  Handle predicate symbol application
 > F t > r  Handle formula
 Eliminate formulae




:: Copointed (Term0 (T t)) (t (Term0 (T t)))   => String > r  Handle string literal
 > Double > r  Handle number literal
 > V > r  Handle variable
 > AtomicWord > [T t] > r  Handle function symbol application
 > T t > r  Handle term
 Eliminate terms



Produced by Haddock version 2.4.2 