| Copyright | (c) Evgenii Kotelnikov 2019-2021 |
|---|---|
| License | GPL-3 |
| Maintainer | evgeny.kotelnikov@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.TPTP
Description
The syntax of the TPTP language. See the BNF grammar definition of TPTP 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))
- unitClause :: (Sign, Literal) -> Clause
- 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))
- sortFirstOrder :: UnsortedFirstOrder -> SortedFirstOrder
- unsortFirstOrder :: MonomorphicFirstOrder -> Maybe UnsortedFirstOrder
- type PolymorphicFirstOrder = FirstOrder (Sorted (Either QuantifiedSort TFF1Sort))
- polymorphizeFirstOrder :: MonomorphicFirstOrder -> PolymorphicFirstOrder
- 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 TSTP = TSTP SZS [Unit]
- data Intro
- data Source
- type Status = Either NoSuccess Success
- data SZS = SZS (Maybe Status) (Maybe Dataform)
- newtype SZSOntology a = SZSOntology {
- unwrapSZSOntology :: a
- data Success
- data NoSuccess
- data Dataform
- data Parent = Parent Source [Info]
- data Expression
- data Info
- = Description Atom
- | Iquote Atom
- | Status (Reserved Success)
- | 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.
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 # | |
| 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_]*, 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\''
Instances
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
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 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.
Instances
The standard function symbol in TPTP. Represents an operation in a first-order theory of arithmetic. See http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic for details.
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. See http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic for details.
Constructors
| Tautology |
|
| Falsum |
|
| Distinct |
|
| Less |
|
| Lesseq |
|
| Greater |
|
| Greatereq |
|
| IsInt |
|
| IsRat |
|
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 |
|
| O |
|
| Int |
|
| Real |
|
| Rat |
|
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. |
Arguments
| :: [Var] | Quantified type variables. |
| -> [TFF1Sort] | Sort arguments. |
| -> TFF1Sort | Return sort. |
| -> Type |
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.
unitClause :: (Sign, Literal) -> Clause Source #
Construct a unit clause from a given signed literal.
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 # 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.
sortFirstOrder :: UnsortedFirstOrder -> SortedFirstOrder Source #
Convert a formula in unsorted first-order logic to a formula in sorted monomorphic first-order logic trivially by omitting the sort annotations in all of its quantifiers. This function always succeeds.
unsortFirstOrder :: MonomorphicFirstOrder -> Maybe UnsortedFirstOrder Source #
Attempt to erase the sort annotations in a sorted monomorphic first-order formula. This function succeeds iff each of the quantifiers omits the sorts of its variables.
type PolymorphicFirstOrder = FirstOrder (Sorted (Either QuantifiedSort TFF1Sort)) Source #
The formula in sorted polymorphic first-order logic.
polymorphizeFirstOrder :: MonomorphicFirstOrder -> PolymorphicFirstOrder Source #
Polymorphize a sorted monomorphic first-order formula. This function always succeeds.
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 and there are no quantified sorts.
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.
The TSTP output - zero or more TSTP units, possibly annotated with the status of the proof search and the resulting dataform.
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 values of the SZS ontologies of a TPTP text.
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
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 # | |
| Enum Success Source # | |
| Eq Success Source # | |
| Ord Success Source # | |
| Show Success Source # | |
| Pretty Success Source # | |
Defined in Data.TPTP.Pretty | |
| Pretty Status Source # | |
Defined in Data.TPTP.Pretty | |
| Named Success Source # | |
| Named (SZSOntology Success) 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 # | |
| Enum NoSuccess Source # | |
Defined in Data.TPTP Methods succ :: NoSuccess -> NoSuccess # pred :: NoSuccess -> NoSuccess # fromEnum :: NoSuccess -> Int # enumFrom :: NoSuccess -> [NoSuccess] # enumFromThen :: NoSuccess -> NoSuccess -> [NoSuccess] # enumFromTo :: NoSuccess -> NoSuccess -> [NoSuccess] # enumFromThenTo :: NoSuccess -> NoSuccess -> NoSuccess -> [NoSuccess] # | |
| Eq NoSuccess Source # | |
| Ord NoSuccess Source # | |
| Show NoSuccess Source # | |
| Pretty NoSuccess Source # | |
Defined in Data.TPTP.Pretty | |
| Pretty Status Source # | |
Defined in Data.TPTP.Pretty | |
| Named (SZSOntology NoSuccess) 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 # | |
| Enum Dataform Source # | |
| Eq Dataform Source # | |
| Ord Dataform Source # | |
Defined in Data.TPTP | |
| Show Dataform Source # | |
| Pretty Dataform Source # | |
Defined in Data.TPTP.Pretty | |
| Named (SZSOntology Dataform) Source # | |
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