tptp-0.1.1.0: A parser and a pretty printer for the TPTP language

Copyright(c) Evgenii Kotelnikov 2019
LicenseGPL-3
Maintainerevgeny.kotelnikov@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.TPTP

Contents

Description

See the BNF grammar definition of the TPTP language for details.

Synopsis

Languages

data Language Source #

The language of logical formulas available in TPTP.

The languages of TPTP form a hierarchy displayed on the following diagram, where arrows indicate inclusion. E.g. each formula in FOF is syntactically a formula in TFF0, but not the other way around.

CNF --> FOF --> TFF0 --> TFF1

Constructors

CNF_

CNF - the language of clausal normal forms of unsorted first-order logic.

FOF_

FOF - the language of full unsorted first-order logic.

TFF_

TFF - the language of full sorted first-order logic, both monomorphic (TFF0) and polymorphic (TFF1).

Instances
Bounded Language Source # 
Instance details

Defined in Data.TPTP

Enum Language Source # 
Instance details

Defined in Data.TPTP

Eq Language Source # 
Instance details

Defined in Data.TPTP

Ord Language Source # 
Instance details

Defined in Data.TPTP

Show Language Source # 
Instance details

Defined in Data.TPTP

Pretty Language Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Language -> Doc ann #

prettyList :: [Language] -> Doc ann #

Named Language Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Language -> Text Source #

Names

newtype Atom Source #

The atomic word in the TPTP language - a non-empty string of space or visible characters from the ASCII range 0x20 to 0x7E. If the string satisfies the regular expression [a-z][a-zA-Z0-9_]*, then it is displayed in the TPTP language as is, otherwise it is displayed in single quotes with the characters ' and \ escaped using \.

>>> print (pretty (Atom "fxYz42"))
fxYz42
>>> print (pretty (Atom "f-'function symbol'"))
'f-\'function symbol\''

Constructors

Atom Text 
Instances
Eq Atom Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Atom -> Atom -> Bool #

(/=) :: Atom -> Atom -> Bool #

Ord Atom Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Atom -> Atom -> Ordering #

(<) :: Atom -> Atom -> Bool #

(<=) :: Atom -> Atom -> Bool #

(>) :: Atom -> Atom -> Bool #

(>=) :: Atom -> Atom -> Bool #

max :: Atom -> Atom -> Atom #

min :: Atom -> Atom -> Atom #

Show Atom Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Atom -> ShowS #

show :: Atom -> String #

showList :: [Atom] -> ShowS #

IsString Atom Source # 
Instance details

Defined in Data.TPTP

Methods

fromString :: String -> Atom #

Pretty UnitName Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: UnitName -> Doc ann #

prettyList :: [UnitName] -> Doc ann #

Pretty Atom Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Atom -> Doc ann #

prettyList :: [Atom] -> Doc ann #

Pretty (Either Var Atom) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Either Var Atom -> Doc ann #

prettyList :: [Either Var Atom] -> Doc ann #

isValidAtom :: Text -> Bool Source #

Check whether a given string is a valid atom.

>>> isValidAtom ""
False
>>> isValidAtom "\r\n"
False
>>> isValidAtom "fxYz42"
True
>>> isValidAtom "f-'function symbol'"
True

newtype Var Source #

The variable in the TPTP language - a string that satisfies the regular expression [A-Z][a-zA-Z0-9_]*.

Constructors

Var Text 
Instances
Eq Var Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Var -> Var -> Bool #

(/=) :: Var -> Var -> Bool #

Ord Var Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Var -> Var -> Ordering #

(<) :: Var -> Var -> Bool #

(<=) :: Var -> Var -> Bool #

(>) :: Var -> Var -> Bool #

(>=) :: Var -> Var -> Bool #

max :: Var -> Var -> Var #

min :: Var -> Var -> Var #

Show Var Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Var -> ShowS #

show :: Var -> String #

showList :: [Var] -> ShowS #

IsString Var Source # 
Instance details

Defined in Data.TPTP

Methods

fromString :: String -> Var #

Pretty Var Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Var -> Doc ann #

prettyList :: [Var] -> Doc ann #

Pretty (Either Var Atom) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Either Var Atom -> Doc ann #

prettyList :: [Either Var Atom] -> Doc ann #

isValidVar :: Text -> Bool Source #

Check whether a given string is a valid variable.

>>> isValidVar ""
False
>>> isValidVar "x"
False
>>> isValidVar "X"
True
>>> isValidVar "Cat"
True
>>> isValidVar "C@t"
False

newtype DistinctObject Source #

The distinct object in the TPTP language - a (possibly empty) string of space or visible characters from the ASCII range 0x20 to 0x7E. The string is always displayed in the TPTP language in double quotes with the characters " and \ escaped using \.

>>> print (pretty (DistinctObject "Godel's incompleteness theorem"))
"Godel's incompleteness theorem"

Distinct objects are different from atoms in that they implicitly carry semantic inequality. The TPTP documentation says the following about distinct objects.

Distinct objects are different from (but may be equal to) other tokens, e.g., "cat" is different from 'cat' and cat. Distinct objects are always interpreted as themselves, so if they are different they are unequal, e.g., "Apple" != "Microsoft" is implicit.

Constructors

DistinctObject Text 

isValidDistinctObject :: Text -> Bool Source #

Check whether a given string is a valid distinct object.

>>> isValidDistinctObject ""
True
>>> isValidDistinctObject "Godel's incompleteness theorem"
True
>>> isValidDistinctObject "\r\n"
False

data Reserved s Source #

The identifier reserved in the TPTP specification and theorem proving systems that implement it. Reserved identifiers are used to represent function symbols, predicate symbols, sorts, formula roles and others. Reserved identifiers are non-empty strings that satisfy the regular expression [a-z][a-zA-Z0-9_]*. Reserved identifiers of functions, predicates, and sorts, used as names, are in addition prepended by $.

>>> print (pretty (Standard I))
i
>>> print (pretty (Standard Axiom))
axiom
>>> print (pretty (Extended "negated_lemma" :: Reserved Role))
negated_lemma

Constructors

Standard s

The identifier contained in the TPTP specification.

Extended Text

The identifier not contained in the standard TPTP but implemented by some theorem prover. For example, Vampire implements the sort constructor $array.

Instances
Eq s => Eq (Reserved s) Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Reserved s -> Reserved s -> Bool #

(/=) :: Reserved s -> Reserved s -> Bool #

Ord s => Ord (Reserved s) Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Reserved s -> Reserved s -> Ordering #

(<) :: Reserved s -> Reserved s -> Bool #

(<=) :: Reserved s -> Reserved s -> Bool #

(>) :: Reserved s -> Reserved s -> Bool #

(>=) :: Reserved s -> Reserved s -> Bool #

max :: Reserved s -> Reserved s -> Reserved s #

min :: Reserved s -> Reserved s -> Reserved s #

Show s => Show (Reserved s) Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Reserved s -> ShowS #

show :: Reserved s -> String #

showList :: [Reserved s] -> ShowS #

(Named a, Enum a, Bounded a) => IsString (Reserved a) Source # 
Instance details

Defined in Data.TPTP

Methods

fromString :: String -> Reserved a #

Named s => Pretty (Reserved s) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Reserved s -> Doc ann #

prettyList :: [Reserved s] -> Doc ann #

Named s => Named (Reserved s) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

name :: Reserved s -> Text Source #

extended :: (Named a, Enum a, Bounded a) => Text -> Reserved a Source #

A smart Extended constructor - only uses Extended if the given string does not correspond to any of the standard identifiers.

>>> extended "int" :: Reserved Sort
Standard Int
>>> extended "array" :: Reserved Sort
Extended "array"

isValidReserved :: Text -> Bool Source #

Check whether a given string is a valid reserved identifier.

>>> isValidReserved ""
False
>>> isValidReserved "x"
True
>>> isValidReserved "X"
False
>>> isValidReserved "cat"
True
>>> isValidReserved "c@t"
False
>>> isValidReserved "$int"
False

class Named a where Source #

The class Named allows assigning concrete names to reserved constants in the TPTP language.

Methods

name :: a -> Text Source #

Instances
Named Success Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Success -> Text Source #

Named Intro Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Intro -> Text Source #

Named Role Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Role -> Text Source #

Named Connective Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Connective -> Text Source #

Named Quantifier Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Quantifier -> Text Source #

Named Sign Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Sign -> Text Source #

Named Sort Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Sort -> Text Source #

Named Predicate Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Predicate -> Text Source #

Named Function Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Function -> Text Source #

Named Language Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Language -> Text Source #

Named (SZSOntology Dataform) Source # 
Instance details

Defined in Data.TPTP

Named (SZSOntology NoSuccess) Source # 
Instance details

Defined in Data.TPTP

Named (SZSOntology Success) Source # 
Instance details

Defined in Data.TPTP

Named s => Named (Reserved s) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

name :: Reserved s -> Text Source #

data Function Source #

The standard function symbol in TPTP. Represents an operation in a first-order theory of arithmetic.

Instances
Bounded Function Source # 
Instance details

Defined in Data.TPTP

Enum Function Source # 
Instance details

Defined in Data.TPTP

Eq Function Source # 
Instance details

Defined in Data.TPTP

Ord Function Source # 
Instance details

Defined in Data.TPTP

Show Function Source # 
Instance details

Defined in Data.TPTP

Named Function Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Function -> Text Source #

data Predicate Source #

The standard predicate symbol in TPTP.

data Name s Source #

The name of a function symbol, a predicate symbol, a sort, a formula role or other.

>>> print (pretty (Reserved (Standard I)))
$i
>>> print (pretty (Reserved (Extended "array" :: Reserved Sort)))
$array
>>> print (pretty (Defined (Atom "array") :: Name Sort))
array

Constructors

Reserved (Reserved s)

The name reserved in the TPTP specification. This name is parsed and pretty printed with the leading $ character.

Defined Atom

The name defined by the user.

Instances
Eq s => Eq (Name s) Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Name s -> Name s -> Bool #

(/=) :: Name s -> Name s -> Bool #

Ord s => Ord (Name s) Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Name s -> Name s -> Ordering #

(<) :: Name s -> Name s -> Bool #

(<=) :: Name s -> Name s -> Bool #

(>) :: Name s -> Name s -> Bool #

(>=) :: Name s -> Name s -> Bool #

max :: Name s -> Name s -> Name s #

min :: Name s -> Name s -> Name s #

Show s => Show (Name s) Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Name s -> ShowS #

show :: Name s -> String #

showList :: [Name s] -> ShowS #

IsString (Name s) Source #

The IsString instance of Name opts for using the Defined constructor.

Instance details

Defined in Data.TPTP

Methods

fromString :: String -> Name s #

Named s => Pretty (Name s) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Name s -> Doc ann #

prettyList :: [Name s] -> Doc ann #

Sorts and types

data Sort Source #

The standard sort in TPTP.

Constructors

I

The sort of individuals.

O

The sort of booleans.

Int

The sort of integers.

Real

The sort of real numbers.

Rat

The sort of rational numbers.

Instances
Bounded Sort Source # 
Instance details

Defined in Data.TPTP

Enum Sort Source # 
Instance details

Defined in Data.TPTP

Methods

succ :: Sort -> Sort #

pred :: Sort -> Sort #

toEnum :: Int -> Sort #

fromEnum :: Sort -> Int #

enumFrom :: Sort -> [Sort] #

enumFromThen :: Sort -> Sort -> [Sort] #

enumFromTo :: Sort -> Sort -> [Sort] #

enumFromThenTo :: Sort -> Sort -> Sort -> [Sort] #

Eq Sort Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Sort -> Sort -> Bool #

(/=) :: Sort -> Sort -> Bool #

Ord Sort Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Sort -> Sort -> Ordering #

(<) :: Sort -> Sort -> Bool #

(<=) :: Sort -> Sort -> Bool #

(>) :: Sort -> Sort -> Bool #

(>=) :: Sort -> Sort -> Bool #

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Show Sort Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

Named Sort Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Sort -> Text Source #

data TFF1Sort Source #

The sort in sorted rank-1 polymorphic logic with sort constructors (TFF1) - an application of a sort constructor to zero or more sorts or a sort variable that comes from a sort quantifier. A zero-arity sort application is simply a sort.

Every TFF0 sort is also a TFF1 sort, but not the other way around.

Instances
Eq TFF1Sort Source # 
Instance details

Defined in Data.TPTP

Ord TFF1Sort Source # 
Instance details

Defined in Data.TPTP

Show TFF1Sort Source # 
Instance details

Defined in Data.TPTP

Pretty TFF1Sort Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: TFF1Sort -> Doc ann #

prettyList :: [TFF1Sort] -> Doc ann #

Pretty (Either QuantifiedSort TFF1Sort) Source # 
Instance details

Defined in Data.TPTP.Pretty

monomorphizeTFF1Sort :: TFF1Sort -> Maybe (Name Sort) Source #

Attempt to convert a given TFF1 sort to TFF0. This function succeeds iff the given sort is a sort constructor with zero arity.

data Type Source #

The type of a function or a predicate symbol in a sorted first-order logic (TFF0 or TFF1). Each TFF0 type is also a TFF1 type, but not the other way around.

Constructors

Type [Name Sort] (Name Sort)

The type of a function or a predicate symbol in the sorted monomorphic first-order logic (TFF0). It is a mapping of zero or more sorts to a sort. The empty list of argument sorts marks the type of a constant symbol.

TFF1Type [Var] [TFF1Sort] TFF1Sort

The type of a function or a predicate symbol in the sorted rank-1 polymorphic first-order logic (TFF1). It is a (possibly quantified) mapping of zero or more TFF1 sorts to a TFF1 sort. The empty list of sort variables marks a monomorphic TFF1 type. The empty list of argument sorts marks the type of a constant symbol.

Instances
Eq Type Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Type -> Type -> Bool #

(/=) :: Type -> Type -> Bool #

Ord Type Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Type -> Type -> Ordering #

(<) :: Type -> Type -> Bool #

(<=) :: Type -> Type -> Bool #

(>) :: Type -> Type -> Bool #

(>=) :: Type -> Type -> Bool #

max :: Type -> Type -> Type #

min :: Type -> Type -> Type #

Show Type Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Type -> ShowS #

show :: Type -> String #

showList :: [Type] -> ShowS #

Pretty Type Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Type -> Doc ann #

prettyList :: [Type] -> Doc ann #

tff1Type :: [Var] -> [TFF1Sort] -> TFF1Sort -> Type Source #

A smart constructor of a TFF1 type. tff1Type constructs a TFF0 type with its arguments, if it is possible, and otherwise constructs a TFF1 type.

First-order logic

data Number Source #

The integer, rational, or real constant.

Constructors

IntegerConstant Integer

A positive or negative integer.

RationalConstant Integer Integer

A rational number, represented as a pair of its numerator (positive or negative integer, possibly zero) and denominator (strictly positive non-zero integer).

RealConstant Scientific

A real number, written in the scientific notation.

Instances
Eq Number Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Number -> Number -> Bool #

(/=) :: Number -> Number -> Bool #

Ord Number Source # 
Instance details

Defined in Data.TPTP

Show Number Source # 
Instance details

Defined in Data.TPTP

Pretty Number Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Number -> Doc ann #

prettyList :: [Number] -> Doc ann #

data Term Source #

The term in first-order logic extended with arithmetic.

Constructors

Function (Name Function) [Term]

Application of a function symbol. The empty list of arguments represents a constant function symbol.

Variable Var

A quantified variable.

Number Number

An integer, rational or real constant.

DistinctTerm DistinctObject

A distinct object.

Instances
Eq Term Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Term -> Term -> Bool #

(/=) :: Term -> Term -> Bool #

Ord Term Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Term -> Term -> Ordering #

(<) :: Term -> Term -> Bool #

(<=) :: Term -> Term -> Bool #

(>) :: Term -> Term -> Bool #

(>=) :: Term -> Term -> Bool #

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

Show Term Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

Pretty Term Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Term -> Doc ann #

prettyList :: [Term] -> Doc ann #

data Literal Source #

The literal in first-order logic. The logical tautology is represented as Predicate (Reserved (Standard Tautology)) [] and the logical falsum is represented as Predicate (Reserved (Standard Falsum)) [].

Constructors

Predicate (Name Predicate) [Term]

Application of a predicate symbol.

Equality Term Sign Term

Equality or inequality.

Instances
Eq Literal Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Literal -> Literal -> Bool #

(/=) :: Literal -> Literal -> Bool #

Ord Literal Source # 
Instance details

Defined in Data.TPTP

Show Literal Source # 
Instance details

Defined in Data.TPTP

Pretty Literal Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Literal -> Doc ann #

prettyList :: [Literal] -> Doc ann #

data Sign Source #

The sign of first-order literals and equality.

Constructors

Positive 
Negative 
Instances
Bounded Sign Source # 
Instance details

Defined in Data.TPTP

Enum Sign Source # 
Instance details

Defined in Data.TPTP

Methods

succ :: Sign -> Sign #

pred :: Sign -> Sign #

toEnum :: Int -> Sign #

fromEnum :: Sign -> Int #

enumFrom :: Sign -> [Sign] #

enumFromThen :: Sign -> Sign -> [Sign] #

enumFromTo :: Sign -> Sign -> [Sign] #

enumFromThenTo :: Sign -> Sign -> Sign -> [Sign] #

Eq Sign Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Sign -> Sign -> Bool #

(/=) :: Sign -> Sign -> Bool #

Ord Sign Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Sign -> Sign -> Ordering #

(<) :: Sign -> Sign -> Bool #

(<=) :: Sign -> Sign -> Bool #

(>) :: Sign -> Sign -> Bool #

(>=) :: Sign -> Sign -> Bool #

max :: Sign -> Sign -> Sign #

min :: Sign -> Sign -> Sign #

Show Sign Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Sign -> ShowS #

show :: Sign -> String #

showList :: [Sign] -> ShowS #

Pretty Sign Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Sign -> Doc ann #

prettyList :: [Sign] -> Doc ann #

Named Sign Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Sign -> Text Source #

newtype Clause Source #

The clause in first-order logic - implicitly universally-quantified disjunction of one or more signed literals. Semantically, a clause is allowed to be empty in which case it is the logical falsum. However, the TPTP syntax does not allow empty clauses, instead the unit clause $false must be used.

Constructors

Clause (NonEmpty (Sign, Literal)) 
Instances
Eq Clause Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Clause -> Clause -> Bool #

(/=) :: Clause -> Clause -> Bool #

Ord Clause Source # 
Instance details

Defined in Data.TPTP

Show Clause Source # 
Instance details

Defined in Data.TPTP

Pretty Clause Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Clause -> Doc ann #

prettyList :: [Clause] -> Doc ann #

clause :: [(Sign, Literal)] -> Clause Source #

A smart constructor for Clause. clause constructs a clause from a possibly empty list of signed literals. If the provided list is empty, the unit clause $false is constructed instead.

data Quantifier Source #

The quantifier in first-order logic.

Constructors

Forall

The universal quantifier.

Exists

The existential quantifier.

Instances
Bounded Quantifier Source # 
Instance details

Defined in Data.TPTP

Enum Quantifier Source # 
Instance details

Defined in Data.TPTP

Eq Quantifier Source # 
Instance details

Defined in Data.TPTP

Ord Quantifier Source # 
Instance details

Defined in Data.TPTP

Show Quantifier Source # 
Instance details

Defined in Data.TPTP

Pretty Quantifier Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Quantifier -> Doc ann #

prettyList :: [Quantifier] -> Doc ann #

Named Quantifier Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Quantifier -> Text Source #

data Connective Source #

The connective in full first-order logic.

Instances
Bounded Connective Source # 
Instance details

Defined in Data.TPTP

Enum Connective Source # 
Instance details

Defined in Data.TPTP

Eq Connective Source # 
Instance details

Defined in Data.TPTP

Ord Connective Source # 
Instance details

Defined in Data.TPTP

Show Connective Source # 
Instance details

Defined in Data.TPTP

Pretty Connective Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Connective -> Doc ann #

prettyList :: [Connective] -> Doc ann #

Named Connective Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Connective -> Text Source #

isAssociative :: Connective -> Bool Source #

Check associativity of a given connective.

>>> isAssociative Implication
False
>>> isAssociative Conjunction
True

data FirstOrder s Source #

The formula in sorted or unsorted first-order logic. Syntactically, the difference between sorted and unsorted formulas is that quantified variables in the former might be annotated with their respective sorts. The type parameter s represents the sort annotation - it is empty for unsorted logic and non-empty for sorted logic.

Instances
Functor FirstOrder Source # 
Instance details

Defined in Data.TPTP

Methods

fmap :: (a -> b) -> FirstOrder a -> FirstOrder b #

(<$) :: a -> FirstOrder b -> FirstOrder a #

Foldable FirstOrder Source # 
Instance details

Defined in Data.TPTP

Methods

fold :: Monoid m => FirstOrder m -> m #

foldMap :: Monoid m => (a -> m) -> FirstOrder a -> m #

foldr :: (a -> b -> b) -> b -> FirstOrder a -> b #

foldr' :: (a -> b -> b) -> b -> FirstOrder a -> b #

foldl :: (b -> a -> b) -> b -> FirstOrder a -> b #

foldl' :: (b -> a -> b) -> b -> FirstOrder a -> b #

foldr1 :: (a -> a -> a) -> FirstOrder a -> a #

foldl1 :: (a -> a -> a) -> FirstOrder a -> a #

toList :: FirstOrder a -> [a] #

null :: FirstOrder a -> Bool #

length :: FirstOrder a -> Int #

elem :: Eq a => a -> FirstOrder a -> Bool #

maximum :: Ord a => FirstOrder a -> a #

minimum :: Ord a => FirstOrder a -> a #

sum :: Num a => FirstOrder a -> a #

product :: Num a => FirstOrder a -> a #

Traversable FirstOrder Source # 
Instance details

Defined in Data.TPTP

Methods

traverse :: Applicative f => (a -> f b) -> FirstOrder a -> f (FirstOrder b) #

sequenceA :: Applicative f => FirstOrder (f a) -> f (FirstOrder a) #

mapM :: Monad m => (a -> m b) -> FirstOrder a -> m (FirstOrder b) #

sequence :: Monad m => FirstOrder (m a) -> m (FirstOrder a) #

Eq s => Eq (FirstOrder s) Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: FirstOrder s -> FirstOrder s -> Bool #

(/=) :: FirstOrder s -> FirstOrder s -> Bool #

Ord s => Ord (FirstOrder s) Source # 
Instance details

Defined in Data.TPTP

Show s => Show (FirstOrder s) Source # 
Instance details

Defined in Data.TPTP

Pretty s => Pretty (FirstOrder s) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: FirstOrder s -> Doc ann #

prettyList :: [FirstOrder s] -> Doc ann #

quantified :: Quantifier -> [(Var, s)] -> FirstOrder s -> FirstOrder s Source #

A smart constructor for Quantified - constructs a quantified first-order formula with a possibly empty list of variables under the quantifier. If the provided list is empty, the underlying formula is returned instead.

newtype Unsorted Source #

The (empty) sort annotation in unsorted first-order logic.

Constructors

Unsorted () 
Instances
Eq Unsorted Source # 
Instance details

Defined in Data.TPTP

Ord Unsorted Source # 
Instance details

Defined in Data.TPTP

Show Unsorted Source # 
Instance details

Defined in Data.TPTP

Pretty Unsorted Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Unsorted -> Doc ann #

prettyList :: [Unsorted] -> Doc ann #

newtype Sorted s Source #

The sort annotation in sorted first-order logic. The TPTP language allows a sort annotation to be omitted, in such case the sort of the variable is assumed to be $i.

Constructors

Sorted (Maybe s) 
Instances
Functor Sorted Source # 
Instance details

Defined in Data.TPTP

Methods

fmap :: (a -> b) -> Sorted a -> Sorted b #

(<$) :: a -> Sorted b -> Sorted a #

Foldable Sorted Source # 
Instance details

Defined in Data.TPTP

Methods

fold :: Monoid m => Sorted m -> m #

foldMap :: Monoid m => (a -> m) -> Sorted a -> m #

foldr :: (a -> b -> b) -> b -> Sorted a -> b #

foldr' :: (a -> b -> b) -> b -> Sorted a -> b #

foldl :: (b -> a -> b) -> b -> Sorted a -> b #

foldl' :: (b -> a -> b) -> b -> Sorted a -> b #

foldr1 :: (a -> a -> a) -> Sorted a -> a #

foldl1 :: (a -> a -> a) -> Sorted a -> a #

toList :: Sorted a -> [a] #

null :: Sorted a -> Bool #

length :: Sorted a -> Int #

elem :: Eq a => a -> Sorted a -> Bool #

maximum :: Ord a => Sorted a -> a #

minimum :: Ord a => Sorted a -> a #

sum :: Num a => Sorted a -> a #

product :: Num a => Sorted a -> a #

Traversable Sorted Source # 
Instance details

Defined in Data.TPTP

Methods

traverse :: Applicative f => (a -> f b) -> Sorted a -> f (Sorted b) #

sequenceA :: Applicative f => Sorted (f a) -> f (Sorted a) #

mapM :: Monad m => (a -> m b) -> Sorted a -> m (Sorted b) #

sequence :: Monad m => Sorted (m a) -> m (Sorted a) #

Eq s => Eq (Sorted s) Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Sorted s -> Sorted s -> Bool #

(/=) :: Sorted s -> Sorted s -> Bool #

Ord s => Ord (Sorted s) Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Sorted s -> Sorted s -> Ordering #

(<) :: Sorted s -> Sorted s -> Bool #

(<=) :: Sorted s -> Sorted s -> Bool #

(>) :: Sorted s -> Sorted s -> Bool #

(>=) :: Sorted s -> Sorted s -> Bool #

max :: Sorted s -> Sorted s -> Sorted s #

min :: Sorted s -> Sorted s -> Sorted s #

Show s => Show (Sorted s) Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Sorted s -> ShowS #

show :: Sorted s -> String #

showList :: [Sorted s] -> ShowS #

Pretty s => Pretty (Sorted s) Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Sorted s -> Doc ann #

prettyList :: [Sorted s] -> Doc ann #

type UnsortedFirstOrder = FirstOrder Unsorted Source #

The formula in unsorted first-order logic.

type MonomorphicFirstOrder = FirstOrder (Sorted (Name Sort)) Source #

The formula in sorted monomorphic first-order logic.

type PolymorphicFirstOrder = FirstOrder (Sorted (Either QuantifiedSort TFF1Sort)) Source #

The formula in sorted polymorphic first-order logic.

monomorphizeFirstOrder :: PolymorphicFirstOrder -> Maybe MonomorphicFirstOrder Source #

Attempt to monomorphize a polymorphic sorted first-order formula. This function succeeds iff each of the quantifiers only uses sort constructors with zero arity.

Units

data Formula Source #

The formula in either of the supported TPTP languages.

Instances
Eq Formula Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Formula -> Formula -> Bool #

(/=) :: Formula -> Formula -> Bool #

Ord Formula Source # 
Instance details

Defined in Data.TPTP

Show Formula Source # 
Instance details

Defined in Data.TPTP

Pretty Formula Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Formula -> Doc ann #

prettyList :: [Formula] -> Doc ann #

formulaLanguage :: Formula -> Language Source #

The TPTP language of a given TPTP formula.

data Role Source #

The predefined role of a formula in a derivation. Theorem provers might introduce other roles.

Instances
Bounded Role Source # 
Instance details

Defined in Data.TPTP

Enum Role Source # 
Instance details

Defined in Data.TPTP

Methods

succ :: Role -> Role #

pred :: Role -> Role #

toEnum :: Int -> Role #

fromEnum :: Role -> Int #

enumFrom :: Role -> [Role] #

enumFromThen :: Role -> Role -> [Role] #

enumFromTo :: Role -> Role -> [Role] #

enumFromThenTo :: Role -> Role -> Role -> [Role] #

Eq Role Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Role -> Role -> Bool #

(/=) :: Role -> Role -> Bool #

Ord Role Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Role -> Role -> Ordering #

(<) :: Role -> Role -> Bool #

(<=) :: Role -> Role -> Bool #

(>) :: Role -> Role -> Bool #

(>=) :: Role -> Role -> Bool #

max :: Role -> Role -> Role #

min :: Role -> Role -> Role #

Show Role Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Role -> ShowS #

show :: Role -> String #

showList :: [Role] -> ShowS #

Named Role Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Role -> Text Source #

data Declaration Source #

The logical declaration.

Constructors

Sort Atom Integer

Introduction of a sort contructor. The non-negative integer argument denotes the arity of the constructor. A constructor with zero arity is simply a sort.

Typing Atom Type

Assignment of a type to a symbol.

Formula (Reserved Role) Formula

Logical formula marked with its role.

declarationLanguage :: Declaration -> Language Source #

The TPTP language of a given TPTP declaration.

type UnitName = Either Atom Integer Source #

The name of a unit - either an atom or an integer.

data Unit Source #

The unit of the TPTP input.

Constructors

Include Atom (Maybe (NonEmpty UnitName))

The include statement.

Unit UnitName Declaration (Maybe Annotation)

The named and possibly annotated logical declaration.

Instances
Eq Unit Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Unit -> Unit -> Bool #

(/=) :: Unit -> Unit -> Bool #

Ord Unit Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Unit -> Unit -> Ordering #

(<) :: Unit -> Unit -> Bool #

(<=) :: Unit -> Unit -> Bool #

(>) :: Unit -> Unit -> Bool #

(>=) :: Unit -> Unit -> Bool #

max :: Unit -> Unit -> Unit #

min :: Unit -> Unit -> Unit #

Show Unit Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Unit -> ShowS #

show :: Unit -> String #

showList :: [Unit] -> ShowS #

Pretty Unit Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Unit -> Doc ann #

prettyList :: [Unit] -> Doc ann #

newtype TPTP Source #

The TPTP input - zero or more TPTP units.

Constructors

TPTP 

Fields

Instances
Eq TPTP Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: TPTP -> TPTP -> Bool #

(/=) :: TPTP -> TPTP -> Bool #

Ord TPTP Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: TPTP -> TPTP -> Ordering #

(<) :: TPTP -> TPTP -> Bool #

(<=) :: TPTP -> TPTP -> Bool #

(>) :: TPTP -> TPTP -> Bool #

(>=) :: TPTP -> TPTP -> Bool #

max :: TPTP -> TPTP -> TPTP #

min :: TPTP -> TPTP -> TPTP #

Show TPTP Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> TPTP -> ShowS #

show :: TPTP -> String #

showList :: [TPTP] -> ShowS #

Pretty TPTP Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: TPTP -> Doc ann #

prettyList :: [TPTP] -> Doc ann #

data TSTP Source #

The TSTP output - zero or more TSTP units, possibly annotated with the status of the proof search and the resulting dataform.

Constructors

TSTP SZS [Unit] 
Instances
Eq TSTP Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: TSTP -> TSTP -> Bool #

(/=) :: TSTP -> TSTP -> Bool #

Ord TSTP Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: TSTP -> TSTP -> Ordering #

(<) :: TSTP -> TSTP -> Bool #

(<=) :: TSTP -> TSTP -> Bool #

(>) :: TSTP -> TSTP -> Bool #

(>=) :: TSTP -> TSTP -> Bool #

max :: TSTP -> TSTP -> TSTP #

min :: TSTP -> TSTP -> TSTP #

Show TSTP Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> TSTP -> ShowS #

show :: TSTP -> String #

showList :: [TSTP] -> ShowS #

Pretty TSTP Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: TSTP -> Doc ann #

prettyList :: [TSTP] -> Doc ann #

Annotations

data Intro Source #

The marking of the way a formula is introduced in a TSTP proof. TPTP recognizes several standard intros and theorem proving systems might use other ones.

Instances
Bounded Intro Source # 
Instance details

Defined in Data.TPTP

Enum Intro Source # 
Instance details

Defined in Data.TPTP

Eq Intro Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Intro -> Intro -> Bool #

(/=) :: Intro -> Intro -> Bool #

Ord Intro Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Intro -> Intro -> Ordering #

(<) :: Intro -> Intro -> Bool #

(<=) :: Intro -> Intro -> Bool #

(>) :: Intro -> Intro -> Bool #

(>=) :: Intro -> Intro -> Bool #

max :: Intro -> Intro -> Intro #

min :: Intro -> Intro -> Intro #

Show Intro Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Intro -> ShowS #

show :: Intro -> String #

showList :: [Intro] -> ShowS #

Pretty Intro Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Intro -> Doc ann #

prettyList :: [Intro] -> Doc ann #

Named Intro Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Intro -> Text Source #

data Source Source #

The source of a unit in a TSTP proof. Most commonly a formula is either defined in a File or is the result of an Inference.

Instances
Eq Source Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Source -> Source -> Bool #

(/=) :: Source -> Source -> Bool #

Ord Source Source # 
Instance details

Defined in Data.TPTP

Show Source Source # 
Instance details

Defined in Data.TPTP

Pretty Source Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Source -> Doc ann #

prettyList :: [Source] -> Doc ann #

type Status = Either NoSuccess Success Source #

The status of the proof search.

data SZS Source #

The status values of the SZS ontologies of a TPTP text.

Constructors

SZS (Maybe Status) (Maybe Dataform) 
Instances
Eq SZS Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: SZS -> SZS -> Bool #

(/=) :: SZS -> SZS -> Bool #

Ord SZS Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: SZS -> SZS -> Ordering #

(<) :: SZS -> SZS -> Bool #

(<=) :: SZS -> SZS -> Bool #

(>) :: SZS -> SZS -> Bool #

(>=) :: SZS -> SZS -> Bool #

max :: SZS -> SZS -> SZS #

min :: SZS -> SZS -> SZS #

Show SZS Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> SZS -> ShowS #

show :: SZS -> String #

showList :: [SZS] -> ShowS #

Semigroup SZS Source # 
Instance details

Defined in Data.TPTP.Parse.Combinators

Methods

(<>) :: SZS -> SZS -> SZS #

sconcat :: NonEmpty SZS -> SZS #

stimes :: Integral b => b -> SZS -> SZS #

Monoid SZS Source # 
Instance details

Defined in Data.TPTP.Parse.Combinators

Methods

mempty :: SZS #

mappend :: SZS -> SZS -> SZS #

mconcat :: [SZS] -> SZS #

newtype SZSOntology a Source #

The auxiliary wrapper used to provide Named instances with full names of SZS ontologies to Success, NoSuccess and Dataform.

Constructors

SZSOntology 

Fields

Instances
Bounded a => Bounded (SZSOntology a) Source # 
Instance details

Defined in Data.TPTP

Enum a => Enum (SZSOntology a) Source # 
Instance details

Defined in Data.TPTP

Eq a => Eq (SZSOntology a) Source # 
Instance details

Defined in Data.TPTP

Ord a => Ord (SZSOntology a) Source # 
Instance details

Defined in Data.TPTP

Show a => Show (SZSOntology a) Source # 
Instance details

Defined in Data.TPTP

Named (SZSOntology Dataform) Source # 
Instance details

Defined in Data.TPTP

Named (SZSOntology NoSuccess) Source # 
Instance details

Defined in Data.TPTP

Named (SZSOntology Success) Source # 
Instance details

Defined in Data.TPTP

data Success Source #

The SZS Success ontology. Values of this ontology are used to mark the result of the proof search and also the status of an inference in a TSTP proof. See The SZS Ontologies for details.

Constructors

SUC

Success.

UNP

UnsatisfiabilityPreserving.

SAP

SatisfiabilityPreserving.

ESA

EquiSatisfiable.

SAT

Satisfiable.

FSA

FinitelySatisfiable.

THM

Theorem.

EQV

Equivalent.

TAC

TautologousConclusion.

WEC

WeakerConclusion.

ETH

EquivalentTheorem.

TAU

Tautology.

WTC

WeakerTautologousConclusion.

WTH

WeakerTheorem.

CAX

ContradictoryAxioms.

SCA

SatisfiableConclusionContradictoryAxioms.

TCA

TautologousConclusionContradictoryAxioms.

WCA

WeakerConclusionContradictoryAxioms.

CUP

CounterUnsatisfiabilityPreserving.

CSP

CounterSatisfiabilityPreserving.

ECS

EquiCounterSatisfiable.

CSA

CounterSatisfiable.

CTH

CounterTheorem.

CEQ

CounterEquivalent.

UNC

UnsatisfiableConclusion.

WCC

WeakerCounterConclusion.

ECT

EquivalentCounterTheorem.

FUN

FinitelyUnsatisfiable.

UNS

Unsatisfiable.

WUC

WeakerUnsatisfiableConclusion.

WCT

WeakerCounterTheorem.

SCC

SatisfiableCounterConclusionContradictoryAxioms.

UCA

UnsatisfiableConclusionContradictoryAxioms.

NOC

NoConsequence.

Instances
Bounded Success Source # 
Instance details

Defined in Data.TPTP

Enum Success Source # 
Instance details

Defined in Data.TPTP

Eq Success Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Success -> Success -> Bool #

(/=) :: Success -> Success -> Bool #

Ord Success Source # 
Instance details

Defined in Data.TPTP

Show Success Source # 
Instance details

Defined in Data.TPTP

Pretty Success Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Success -> Doc ann #

prettyList :: [Success] -> Doc ann #

Pretty Status Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Status -> Doc ann #

prettyList :: [Status] -> Doc ann #

Named Success Source # 
Instance details

Defined in Data.TPTP

Methods

name :: Success -> Text Source #

Named (SZSOntology Success) Source # 
Instance details

Defined in Data.TPTP

data NoSuccess Source #

The SZS NoSuccess ontology. Values of this ontology are used to mark the result of the proof search. See The SZS Ontologies for details.

Constructors

NOS

NoSuccess.

OPN

Open.

UNK

Unknown.

ASS

Assumed.

STP

Stopped.

ERR

Error.

OSE

OSError.

INE

InputError.

USE

UsageError.

SYE

SyntaxError.

SEE

SemanticError.

TYE

TypeError.

FOR

Forced.

USR

User.

RSO

ResourceOut.

TMO

Timeout.

MMO

MemoryOut.

GUP

GaveUp.

INC

Incomplete.

IAP

Inappropriate.

INP

InProgress.

NTT

NotTried.

NTY

NotTriedYet.

Instances
Bounded NoSuccess Source # 
Instance details

Defined in Data.TPTP

Enum NoSuccess Source # 
Instance details

Defined in Data.TPTP

Eq NoSuccess Source # 
Instance details

Defined in Data.TPTP

Ord NoSuccess Source # 
Instance details

Defined in Data.TPTP

Show NoSuccess Source # 
Instance details

Defined in Data.TPTP

Pretty NoSuccess Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: NoSuccess -> Doc ann #

prettyList :: [NoSuccess] -> Doc ann #

Pretty Status Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Status -> Doc ann #

prettyList :: [Status] -> Doc ann #

Named (SZSOntology NoSuccess) Source # 
Instance details

Defined in Data.TPTP

data Dataform Source #

The SZS Dataform ontology. Values of this ontology are used to mark the form of logical data produced during proof search. See The SZS Ontologies for details.

Constructors

LDa

LogicalData.

Sln

Solution.

Prf

Proof.

Der

Derivation.

Ref

Refutation.

CRf

CNFRefutation.

Int_

Interpretation.

Mod

Model.

Pin

PartialInterpretation.

PMo

PartialModel.

SIn

StrictlyPartialInterpretation.

SMo

StrictlyPartialModel.

DIn

DomainInterpretation.

DMo

DomainModel.

DPI

DomainPartialInterpretation.

DPM

DomainPartialModel.

DSI

DomainStrictlyPartialInterpretation.

DSM

DomainStrictlyPartialModel.

FIn

FiniteInterpretation.

FMo

FiniteModel.

FPI

FinitePartialInterpretation.

FPM

FinitePartialModel.

FSI

FiniteStrictlyPartialInterpretation.

FSM

FiniteStrictlyPartialModel.

HIn

HerbrandInterpretation.

HMo

HerbrandModel.

TIn

FormulaInterpretation.

TMo

FormulaModel.

TPI

FormulaPartialInterpretation.

TSI

FormulaStrictlyPartialInterpretation.

TSM

FormulaStrictlyPartialModel.

Sat

Saturation.

Lof

ListOfFormulae.

Lth

ListOfTHF.

Ltf

ListOfTFF.

Lfo

ListOfFOF.

Lcn

ListOfCNF.

NSo

NotASolution.

Ass

Assurance.

IPr

IncompleteProof.

IIn

IncompleteInterpretation.

Non

None.

Instances
Bounded Dataform Source # 
Instance details

Defined in Data.TPTP

Enum Dataform Source # 
Instance details

Defined in Data.TPTP

Eq Dataform Source # 
Instance details

Defined in Data.TPTP

Ord Dataform Source # 
Instance details

Defined in Data.TPTP

Show Dataform Source # 
Instance details

Defined in Data.TPTP

Pretty Dataform Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Dataform -> Doc ann #

prettyList :: [Dataform] -> Doc ann #

Named (SZSOntology Dataform) Source # 
Instance details

Defined in Data.TPTP

data Parent Source #

The parent of a formula in an inference.

Constructors

Parent Source [Info] 
Instances
Eq Parent Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Parent -> Parent -> Bool #

(/=) :: Parent -> Parent -> Bool #

Ord Parent Source # 
Instance details

Defined in Data.TPTP

Show Parent Source # 
Instance details

Defined in Data.TPTP

Pretty Parent Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Parent -> Doc ann #

prettyList :: [Parent] -> Doc ann #

data Expression Source #

An expression is either a formula or a term. Expressions occur in TSTP proofs.

Constructors

Logical Formula 
Term Term 
Instances
Eq Expression Source # 
Instance details

Defined in Data.TPTP

Ord Expression Source # 
Instance details

Defined in Data.TPTP

Show Expression Source # 
Instance details

Defined in Data.TPTP

Pretty Expression Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Expression -> Doc ann #

prettyList :: [Expression] -> Doc ann #

data Info Source #

The information about a formula.

Instances
Eq Info Source # 
Instance details

Defined in Data.TPTP

Methods

(==) :: Info -> Info -> Bool #

(/=) :: Info -> Info -> Bool #

Ord Info Source # 
Instance details

Defined in Data.TPTP

Methods

compare :: Info -> Info -> Ordering #

(<) :: Info -> Info -> Bool #

(<=) :: Info -> Info -> Bool #

(>) :: Info -> Info -> Bool #

(>=) :: Info -> Info -> Bool #

max :: Info -> Info -> Info #

min :: Info -> Info -> Info #

Show Info Source # 
Instance details

Defined in Data.TPTP

Methods

showsPrec :: Int -> Info -> ShowS #

show :: Info -> String #

showList :: [Info] -> ShowS #

Pretty Info Source # 
Instance details

Defined in Data.TPTP.Pretty

Methods

pretty :: Info -> Doc ann #

prettyList :: [Info] -> Doc ann #

type Annotation = (Source, Maybe [Info]) Source #

The annotation of a unit. Most commonly, annotations are attached to units in TSTP proofs.