| Copyright | (c) Evgenii Kotelnikov 2019 |
|---|---|
| License | GPL-3 |
| Maintainer | evgeny.kotelnikov@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.TPTP
Description
See the BNF grammar definition of the TPTP language for details.
Synopsis
- data Language
- newtype Atom = Atom Text
- isValidAtom :: Text -> Bool
- newtype Var = Var Text
- isValidVar :: Text -> Bool
- newtype DistinctObject = DistinctObject Text
- isValidDistinctObject :: Text -> Bool
- data Reserved s
- extended :: (Named a, Enum a, Bounded a) => Text -> Reserved a
- isValidReserved :: Text -> Bool
- class Named a where
- data Function
- = Uminus
- | Sum
- | Difference
- | Product
- | Quotient
- | QuotientE
- | QuotientT
- | QuotientF
- | RemainderE
- | RemainderT
- | RemainderF
- | Floor
- | Ceiling
- | Truncate
- | Round
- | ToInt
- | ToRat
- | ToReal
- data Predicate
- data Name s
- data Sort
- data TFF1Sort
- monomorphizeTFF1Sort :: TFF1Sort -> Maybe (Name Sort)
- data Type
- tff1Type :: [Var] -> [TFF1Sort] -> TFF1Sort -> Type
- data Number
- data Term
- data Literal
- data Sign
- newtype Clause = Clause (NonEmpty (Sign, Literal))
- clause :: [(Sign, Literal)] -> Clause
- data Quantifier
- data Connective
- isAssociative :: Connective -> Bool
- data FirstOrder s
- = Atomic Literal
- | Negated (FirstOrder s)
- | Connected (FirstOrder s) Connective (FirstOrder s)
- | Quantified Quantifier (NonEmpty (Var, s)) (FirstOrder s)
- quantified :: Quantifier -> [(Var, s)] -> FirstOrder s -> FirstOrder s
- newtype Unsorted = Unsorted ()
- newtype Sorted s = Sorted (Maybe s)
- newtype QuantifiedSort = QuantifiedSort ()
- type UnsortedFirstOrder = FirstOrder Unsorted
- type SortedFirstOrder = MonomorphicFirstOrder
- type MonomorphicFirstOrder = FirstOrder (Sorted (Name Sort))
- type PolymorphicFirstOrder = FirstOrder (Sorted (Either QuantifiedSort TFF1Sort))
- monomorphizeFirstOrder :: PolymorphicFirstOrder -> Maybe MonomorphicFirstOrder
- data Formula
- formulaLanguage :: Formula -> Language
- data Role
- data Declaration
- declarationLanguage :: Declaration -> Language
- type UnitName = Either Atom Integer
- data Unit
- = Include Atom (Maybe (NonEmpty UnitName))
- | Unit UnitName Declaration (Maybe Annotation)
- newtype TPTP = TPTP {}
- data Intro
- data Source
- data Status
- data Parent = Parent Source [Info]
- data Expression
- data Info
- = Description Atom
- | Iquote Atom
- | Status (Reserved Status)
- | Assumptions (NonEmpty UnitName)
- | NewSymbols Atom [Either Var Atom]
- | Refutation Atom
- | Expression Expression
- | Bind Var Expression
- | Application Atom [Info]
- | InfoNumber Number
- | Infos [Info]
- type Annotation = (Source, Maybe [Info])
Languages
The language of logical formulas available in TPTP.
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 # | |
| Enum Language Source # | |
| Eq Language Source # | |
| Ord Language Source # | |
Defined in Data.TPTP | |
| Show Language Source # | |
| Pretty Language Source # | |
Defined in Data.TPTP.Pretty | |
| Named Language Source # | |
Names
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_]* 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\''
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
The variable in the TPTP language - a string that satisfies the regular
expression [A-Z][a-zA-Z0-9_]*.
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 |
Instances
| Eq DistinctObject Source # | |
Defined in Data.TPTP Methods (==) :: DistinctObject -> DistinctObject -> Bool # (/=) :: DistinctObject -> DistinctObject -> Bool # | |
| Ord DistinctObject Source # | |
Defined in Data.TPTP Methods compare :: DistinctObject -> DistinctObject -> Ordering # (<) :: DistinctObject -> DistinctObject -> Bool # (<=) :: DistinctObject -> DistinctObject -> Bool # (>) :: DistinctObject -> DistinctObject -> Bool # (>=) :: DistinctObject -> DistinctObject -> Bool # max :: DistinctObject -> DistinctObject -> DistinctObject # min :: DistinctObject -> DistinctObject -> DistinctObject # | |
| Show DistinctObject Source # | |
Defined in Data.TPTP Methods showsPrec :: Int -> DistinctObject -> ShowS # show :: DistinctObject -> String # showList :: [DistinctObject] -> ShowS # | |
| IsString DistinctObject Source # | |
Defined in Data.TPTP Methods fromString :: String -> DistinctObject # | |
| Pretty DistinctObject Source # | |
Defined in Data.TPTP.Pretty | |
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
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 uses the sort constructor |
Instances
| Eq s => Eq (Reserved s) Source # | |
| Ord s => Ord (Reserved s) Source # | |
| Show s => Show (Reserved s) Source # | |
| (Named a, Enum a, Bounded a) => IsString (Reserved a) Source # | |
Defined in Data.TPTP Methods fromString :: String -> Reserved a # | |
| Named s => Pretty (Reserved s) Source # | |
Defined in Data.TPTP.Pretty | |
| Named s => Named (Reserved s) Source # | |
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
The class Named allows assigning concrete names to reserved constants
in the TPTP language.
The standard function symbol in TPTP. Represents an operation in a first-order theory of arithmetic.
Constructors
| Uminus | |
| Sum | |
| Difference | |
| Product | |
| Quotient | |
| QuotientE | |
| QuotientT | |
| QuotientF | |
| RemainderE | |
| RemainderT | |
| RemainderF | |
| Floor | |
| Ceiling | |
| Truncate | |
| Round | |
| ToInt | |
| ToRat | |
| ToReal |
Instances
| Bounded Function Source # | |
| Enum Function Source # | |
| Eq Function Source # | |
| Ord Function Source # | |
Defined in Data.TPTP | |
| Show Function Source # | |
| Named Function Source # | |
The standard predicate symbol in TPTP.
Instances
| Bounded Predicate Source # | |
| Enum Predicate Source # | |
Defined in Data.TPTP Methods succ :: Predicate -> Predicate # pred :: Predicate -> Predicate # fromEnum :: Predicate -> Int # enumFrom :: Predicate -> [Predicate] # enumFromThen :: Predicate -> Predicate -> [Predicate] # enumFromTo :: Predicate -> Predicate -> [Predicate] # enumFromThenTo :: Predicate -> Predicate -> Predicate -> [Predicate] # | |
| Eq Predicate Source # | |
| Ord Predicate Source # | |
| Show Predicate Source # | |
| Named Predicate 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 |
| Defined Atom | The name defined by the user. |
Instances
| Eq s => Eq (Name s) Source # | |
| Ord s => Ord (Name s) Source # | |
| Show s => Show (Name s) Source # | |
| IsString (Name s) Source # | The |
Defined in Data.TPTP Methods fromString :: String -> Name s # | |
| Named s => Pretty (Name s) Source # | |
Defined in Data.TPTP.Pretty | |
Sorts and types
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. |
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 # | |
| Ord TFF1Sort Source # | |
Defined in Data.TPTP | |
| Show TFF1Sort Source # | |
| Pretty TFF1Sort Source # | |
Defined in Data.TPTP.Pretty | |
| Pretty (Either QuantifiedSort TFF1Sort) Source # | |
Defined in Data.TPTP.Pretty Methods pretty :: Either QuantifiedSort TFF1Sort -> Doc ann # prettyList :: [Either QuantifiedSort TFF1Sort] -> Doc ann # | |
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.
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. |
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
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. |
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. |
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. |
The sign of first-order literals and equality.
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.
data Quantifier Source #
The quantifier in first-order logic.
Instances
data Connective Source #
The connective in full first-order logic.
Constructors
| Conjunction | |
| Disjunction | |
| Implication | |
| Equivalence | |
| ExclusiveOr | |
| NegatedConjunction | |
| NegatedDisjunction | |
| ReversedImplication |
Instances
isAssociative :: Connective -> Bool Source #
Check associativity of a given connective.
>>>isAssociative ImplicationFalse
>>>isAssociative ConjunctionTrue
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.
Constructors
| Atomic Literal | |
| Negated (FirstOrder s) | |
| Connected (FirstOrder s) Connective (FirstOrder s) | |
| Quantified Quantifier (NonEmpty (Var, s)) (FirstOrder s) |
Instances
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.
The (empty) sort annotation in unsorted first-order logic.
Constructors
| Unsorted () |
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.
Instances
| Functor Sorted Source # | |
| Foldable Sorted Source # | |
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 # elem :: Eq a => a -> Sorted a -> Bool # maximum :: Ord a => Sorted a -> a # minimum :: Ord a => Sorted a -> a # | |
| Traversable Sorted Source # | |
| Eq s => Eq (Sorted s) Source # | |
| Ord s => Ord (Sorted s) Source # | |
Defined in Data.TPTP | |
| Show s => Show (Sorted s) Source # | |
| Pretty s => Pretty (Sorted s) Source # | |
Defined in Data.TPTP.Pretty | |
newtype QuantifiedSort Source #
The marker of quantified sort.
Constructors
| QuantifiedSort () |
Instances
type UnsortedFirstOrder = FirstOrder Unsorted Source #
The formula in unsorted first-order logic.
type SortedFirstOrder = MonomorphicFirstOrder Source #
An alias for MonomorphicFirstOrder.
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
The formula in either of the supported TPTP languages.
formulaLanguage :: Formula -> Language Source #
The TPTP language of a given TPTP formula.
The predefined role of a formula in a derivation. Theorem provers might introduce other roles.
Constructors
| Axiom | |
| Hypothesis | |
| Definition | |
| Assumption | |
| Lemma | |
| Theorem | |
| Corollary | |
| Conjecture | |
| NegatedConjecture | |
| Plain | |
| FiDomain | |
| FiFunctors | |
| FiPredicates | |
| Unknown |
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. |
Instances
| Eq Declaration Source # | |
Defined in Data.TPTP | |
| Ord Declaration Source # | |
Defined in Data.TPTP Methods compare :: Declaration -> Declaration -> Ordering # (<) :: Declaration -> Declaration -> Bool # (<=) :: Declaration -> Declaration -> Bool # (>) :: Declaration -> Declaration -> Bool # (>=) :: Declaration -> Declaration -> Bool # max :: Declaration -> Declaration -> Declaration # min :: Declaration -> Declaration -> Declaration # | |
| Show Declaration Source # | |
Defined in Data.TPTP Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS # | |
| Pretty Declaration Source # | |
Defined in Data.TPTP.Pretty | |
declarationLanguage :: Declaration -> Language Source #
The TPTP language of a given TPTP declaration.
The unit of the TPTP input.
Constructors
| Include Atom (Maybe (NonEmpty UnitName)) | The |
| Unit UnitName Declaration (Maybe Annotation) | The named and possibly annotated logical declaration. |
The TPTP input - zero or more TPTP units.
Annotations
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.
Constructors
| ByDefinition | |
| ByAxiomOfChoice | |
| ByTautology | |
| ByAssumption |
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.
Constructors
| File Atom (Maybe UnitName) | |
| Theory Atom (Maybe [Info]) | |
| Creator Atom (Maybe [Info]) | |
| Introduced (Reserved Intro) (Maybe [Info]) | |
| Inference Atom [Info] [Parent] | |
| UnitSource UnitName | |
| UnknownSource |
The status of an inference. See The SZS Ontologies for details.
Constructors
| SUC | |
| UNP | |
| SAP | |
| ESA | |
| SAT | |
| FSA | |
| THM | |
| EQV | |
| TAC | |
| WEC | |
| ETH | |
| TAU | |
| WTC | |
| WTH | |
| CAX | |
| SCA | |
| TCA | |
| WCA | |
| CUP | |
| CSP | |
| ECS | |
| CSA | |
| CTH | |
| CEQ | |
| UNC | |
| WCC | |
| ECT | |
| FUN | |
| UNS | |
| WUC | |
| WCT | |
| SCC | |
| UCA | |
| NOC |
The parent of a formula in an inference.
data Expression Source #
An expression is either a formula or a term. Expressions occur in TSTP proofs.
Instances
| Eq Expression Source # | |
Defined in Data.TPTP | |
| Ord Expression Source # | |
Defined in Data.TPTP Methods compare :: Expression -> Expression -> Ordering # (<) :: Expression -> Expression -> Bool # (<=) :: Expression -> Expression -> Bool # (>) :: Expression -> Expression -> Bool # (>=) :: Expression -> Expression -> Bool # max :: Expression -> Expression -> Expression # min :: Expression -> Expression -> Expression # | |
| Show Expression Source # | |
Defined in Data.TPTP Methods showsPrec :: Int -> Expression -> ShowS # show :: Expression -> String # showList :: [Expression] -> ShowS # | |
| Pretty Expression Source # | |
Defined in Data.TPTP.Pretty | |
The information about a formula.
Constructors