| Copyright | (c) A. Tsogias, DFKI Bremen 2011 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Alexis.Tsogias@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
THF.As
Description
A Abstract Syntax for the TPTP-THF Input Syntax v5.1.0.2 taken from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html In addition the Syntax for THF0 taken from http://www.ags.uni-sb.de/~chris/papers/C25.pdf P. 15-16 has been added where needed.
Documentation
data TPTP_THF
data Comment
Constructors
| Comment_Line Token | |
| Comment_Block Token |
data DefinedComment
Constructors
| Defined_Comment_Line Token | |
| Defined_Comment_Block Token |
data SystemComment
Constructors
| System_Comment_Line Token | |
| System_Comment_Block Token |
data Include
data Annotations
Constructors
| Annotations Source OptionalInfo | |
| Null |
data FormulaRole
data THFFormula
Constructors
| TF_THF_Logic_Formula THFLogicFormula | |
| TF_THF_Sequent THFSequent | |
| T0F_THF_Typed_Const THFTypedConst |
Instances
data THFLogicFormula
data THFBinaryFormula
data THFBinaryTuple
data THFUnitaryFormula
Constructors
data THFQuantifiedFormula
type THFVariableList = [THFVariable]
data THFVariable
Constructors
| TV_THF_Typed_Variable Token THFTopLevelType | |
| TV_Variable Token |
data THFTypedConst
data THFTypeFormula
data THFTypeableFormula
data THFSubType
Constructors
| TST_THF_Sub_Type Constant Constant |
data THFTopLevelType
data THFUnitaryType
data THFBinaryType
data THFAtom
type THFTuple = [THFLogicFormula]
data THFSequent
Constructors
| TS_THF_Sequent THFTuple THFTuple | |
| TS_THF_Sequent_Par THFSequent |
data THFConnTerm
data THFQuantifier
data Quantifier
Constructors
| T0Q_ForAll | |
| T0Q_Exists |
data THFPairConnective
Constructors
| Infix_Equality | |
| Infix_Inequality | |
| Equivalent | |
| Implication | |
| IF | |
| XOR | |
| NOR | |
| NAND |
data THFUnaryConnective
Constructors
| Negation | |
| PiForAll | |
| SigmaExists |
data AssocConnective
data DefinedType
data DefinedPlainFormula
data DefinedProp
data DefinedPred
data Term
Constructors
| T_Function_Term FunctionTerm | |
| T_Variable Token |
data FunctionTerm
data PlainTerm
Constructors
| PT_Plain_Term AtomicWord Arguments | |
| PT_Constant Constant |
type Constant = AtomicWord
data DefinedTerm
data DefinedAtom
Constructors
| DA_Number Number | |
| DA_Distinct_Object Token |
data DefinedPlainTerm
data DefinedFunctor
data SystemTerm
Constructors
| ST_System_Term Token Arguments | |
| ST_System_Constant Token |
data PrincipalSymbol
Constructors
| PS_Functor AtomicWord | |
| PS_Variable Token |
data Source
data DagSource
Constructors
| DS_Name Name | |
| DS_Inference_Record AtomicWord UsefulInfo [ParentInfo] |
data ParentInfo
Constructors
| PI_Parent_Info Source (Maybe GeneralList) |
data IntroType
Constructors
| IT_definition | |
| IT_axiom_of_choice | |
| IT_tautology | |
| IT_assumption |
data ExternalSource
data FileSource
data TheoryName
type OptionalInfo = Maybe UsefulInfo
type UsefulInfo = [InfoItem]
data InfoItem
data FormulaItem
Constructors
| FI_Description_Item AtomicWord | |
| FI_Iquote_Item AtomicWord |
data InferenceItem
data InferenceStatus
Constructors
| IS_Status StatusValue | |
| IS_Inference_Info AtomicWord AtomicWord GeneralList |
data StatusValue
data GeneralTerm
data GeneralData
data GeneralFunction
Constructors
| GF_General_Function AtomicWord GeneralTerms |
data FormulaData
Constructors
| THF_Formula THFFormula |
type GeneralList = GeneralTerms
type GeneralTerms = [GeneralTerm]
data Name
Constructors
| N_Atomic_Word AtomicWord | |
| N_Integer Token | |
| T0N_Unsigned_Integer Token |
data AtomicWord
Constructors
| A_Lower_Word Token | |
| A_Single_Quoted Token |