Copyright | (c) Eugen Kuksa University of Magdeburg 2017 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Eugen Kuksa <kuksa@iks.cs.ovgu.de> |
Stability | provisional |
Portability | non-portable (imports Logic) |
Safe Haskell | None |
TPTP.Sign
Description
Data structures representing TPTP signatures.
Documentation
type Sentence = Annotated_formula Source #
Constructors
Symbol | |
Fields
|
Instances
Eq Symbol Source # | |
Data Symbol Source # | |
Ord Symbol Source # | |
Show Symbol Source # | |
GetRange Symbol Source # | |
Sentences TPTP Sentence Sign Morphism Symbol Source # | |
Syntax TPTP BASIC_SPEC Symbol () () Source # | |
StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source # | |
Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source # | |
data SymbolType Source #
Constructors
Constant | |
Number | |
Predicate | |
Proposition | |
Function | |
TypeConstant | |
TypeFunctor |
Instances
Eq SymbolType Source # | |
Data SymbolType Source # | |
Ord SymbolType Source # | |
Show SymbolType Source # | |
GetRange SymbolType Source # | |
symbolTypeS :: Symbol -> String Source #
type ConstantSet = Set Constant Source #
type FunctorMap = Map TPTP_functor FunctorType Source #
type PropositionSet = Set Proposition Source #
type THFTypeDeclarationMap = Map THFTypeable THF_top_level_type Source #
type TFFTypeDeclarationMap = Map Untyped_atom TFF_top_level_type Source #
type FOFPredicateMap = Map Predicate (Set Int) Source #
type FOFFunctorMap = Map TPTP_functor (Set Int) Source #
type THFSubTypeMap = Map THF_atom THF_atom Source #
type TFFSubTypeMap = Map Untyped_atom Atom Source #
data THFTypeable Source #
Constructors
THFTypeFormula THF_typeable_formula | |
THFTypeConstant Constant |
Instances
Eq THFTypeable Source # | |
Data THFTypeable Source # | |
Ord THFTypeable Source # | |
Show THFTypeable Source # | |
data FunctorType Source #
Constructors
FunctorTHF THF_arguments | |
FunctorFOF FOF_arguments |
Instances
Eq FunctorType Source # | |
Data FunctorType Source # | |
Ord FunctorType Source # | |
Show FunctorType Source # | |
data PredicateType Source #
Constructors
PredicateType FOF_arguments |
Instances
Eq PredicateType Source # | |
Data PredicateType Source # | |
Ord PredicateType Source # | |
Show PredicateType Source # | |
data Type_functorType Source #
Constructors
Type_functorType TFF_type_arguments |
Instances
Eq Type_functorType Source # | |
Data Type_functorType Source # | |
Ord Type_functorType Source # | |
Show Type_functorType Source # | |
Constructors
Instances
negateSentence :: Sentence -> Maybe Sentence Source #