Hets - the Heterogeneous Tool Set

Copyright(c) Eugen Kuksa University of Magdeburg 2017
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerEugen Kuksa <kuksa@iks.cs.ovgu.de>
Stabilityprovisional
Portabilitynon-portable (imports Logic)
Safe HaskellNone

TPTP.Sign

Description

Data structures representing TPTP signatures.

Documentation

data Symbol Source #

Constructors

Symbol 

Instances

Eq Symbol Source # 

Methods

(==) :: Symbol -> Symbol -> Bool

(/=) :: Symbol -> Symbol -> Bool

Data Symbol Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol

toConstr :: Symbol -> Constr

dataTypeOf :: Symbol -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Symbol)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)

gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r

gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol

Ord Symbol Source # 

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

(<=) :: Symbol -> Symbol -> Bool

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Symbol Source # 

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

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 # 

Methods

basic_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: TPTP -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: TPTP -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: TPTP -> Sign -> [()] -> Result [()] Source #

convertTheory :: TPTP -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source #

ensures_amalgamability :: TPTP -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: TPTP -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: TPTP -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: TPTP -> Symbol -> () Source #

id_to_raw :: TPTP -> Id -> () Source #

matches :: TPTP -> Symbol -> () -> Bool Source #

empty_signature :: TPTP -> Sign Source #

add_symb_to_sign :: TPTP -> Sign -> Symbol -> Result Sign Source #

signature_union :: TPTP -> Sign -> Sign -> Result Sign Source #

signatureDiff :: TPTP -> Sign -> Sign -> Result Sign Source #

intersection :: TPTP -> Sign -> Sign -> Result Sign Source #

final_union :: TPTP -> Sign -> Sign -> Result Sign Source #

morphism_union :: TPTP -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: TPTP -> Sign -> Sign -> Bool Source #

subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism Source #

generated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: TPTP -> EndoMap () -> Sign -> Result Morphism Source #

induced_from_to_morphism :: TPTP -> EndoMap () -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: TPTP -> Morphism -> Bool Source #

is_injective :: TPTP -> Morphism -> Bool Source #

theory_to_taxonomy :: TPTP -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: TPTP -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: TPTP -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: TPTP -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source # 

Methods

parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: TPTP -> Stability Source #

data_logic :: TPTP -> Maybe AnyLogic Source #

top_sublogic :: TPTP -> Sublogic Source #

all_sublogics :: TPTP -> [Sublogic] Source #

bottomSublogic :: TPTP -> Maybe Sublogic Source #

sublogicDimensions :: TPTP -> [[Sublogic]] Source #

parseSublogic :: TPTP -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source #

provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source #

default_prover :: TPTP -> String Source #

cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source #

conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: TPTP -> ProofTree Source #

syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: TPTP -> Maybe OMCD Source #

export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

data SymbolType Source #

Instances

Eq SymbolType Source # 

Methods

(==) :: SymbolType -> SymbolType -> Bool

(/=) :: SymbolType -> SymbolType -> Bool

Data SymbolType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType

toConstr :: SymbolType -> Constr

dataTypeOf :: SymbolType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SymbolType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType)

gmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r

gmapQ :: (forall d. Data d => d -> u) -> SymbolType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType

Ord SymbolType Source # 
Show SymbolType Source # 

Methods

showsPrec :: Int -> SymbolType -> ShowS

show :: SymbolType -> String

showList :: [SymbolType] -> ShowS

GetRange SymbolType Source # 

symbolTypeS :: Symbol -> String Source #

type FOFPredicateMap = Map Predicate (Set Int) Source #

type FOFFunctorMap = Map TPTP_functor (Set Int) Source #

data THFTypeable Source #

Instances

Eq THFTypeable Source # 

Methods

(==) :: THFTypeable -> THFTypeable -> Bool

(/=) :: THFTypeable -> THFTypeable -> Bool

Data THFTypeable Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeable -> c THFTypeable

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeable

toConstr :: THFTypeable -> Constr

dataTypeOf :: THFTypeable -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c THFTypeable)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypeable)

gmapT :: (forall b. Data b => b -> b) -> THFTypeable -> THFTypeable

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r

gmapQ :: (forall d. Data d => d -> u) -> THFTypeable -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> THFTypeable -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable

Ord THFTypeable Source # 
Show THFTypeable Source # 

Methods

showsPrec :: Int -> THFTypeable -> ShowS

show :: THFTypeable -> String

showList :: [THFTypeable] -> ShowS

data FunctorType Source #

Instances

Eq FunctorType Source # 

Methods

(==) :: FunctorType -> FunctorType -> Bool

(/=) :: FunctorType -> FunctorType -> Bool

Data FunctorType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctorType -> c FunctorType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctorType

toConstr :: FunctorType -> Constr

dataTypeOf :: FunctorType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c FunctorType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctorType)

gmapT :: (forall b. Data b => b -> b) -> FunctorType -> FunctorType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r

gmapQ :: (forall d. Data d => d -> u) -> FunctorType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctorType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType

Ord FunctorType Source # 
Show FunctorType Source # 

Methods

showsPrec :: Int -> FunctorType -> ShowS

show :: FunctorType -> String

showList :: [FunctorType] -> ShowS

data PredicateType Source #

Instances

Eq PredicateType Source # 
Data PredicateType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredicateType -> c PredicateType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredicateType

toConstr :: PredicateType -> Constr

dataTypeOf :: PredicateType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PredicateType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredicateType)

gmapT :: (forall b. Data b => b -> b) -> PredicateType -> PredicateType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r

gmapQ :: (forall d. Data d => d -> u) -> PredicateType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PredicateType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType

Ord PredicateType Source # 
Show PredicateType Source # 

Methods

showsPrec :: Int -> PredicateType -> ShowS

show :: PredicateType -> String

showList :: [PredicateType] -> ShowS

data Type_functorType Source #

Instances

Eq Type_functorType Source # 
Data Type_functorType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type_functorType -> c Type_functorType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type_functorType

toConstr :: Type_functorType -> Constr

dataTypeOf :: Type_functorType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Type_functorType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type_functorType)

gmapT :: (forall b. Data b => b -> b) -> Type_functorType -> Type_functorType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r

gmapQ :: (forall d. Data d => d -> u) -> Type_functorType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Type_functorType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType

Ord Type_functorType Source # 
Show Type_functorType Source # 

Methods

showsPrec :: Int -> Type_functorType -> ShowS

show :: Type_functorType -> String

showList :: [Type_functorType] -> ShowS

data Sign Source #

Instances

Eq Sign Source # 

Methods

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

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

Data Sign Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign

toConstr :: Sign -> Constr

dataTypeOf :: Sign -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Sign)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)

gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r

gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign

Ord Sign Source # 

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 # 

Methods

showsPrec :: Int -> Sign -> ShowS

show :: Sign -> String

showList :: [Sign] -> ShowS

Sentences TPTP Sentence Sign Morphism Symbol Source # 
StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source # 

Methods

basic_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: TPTP -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: TPTP -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: TPTP -> Sign -> [()] -> Result [()] Source #

convertTheory :: TPTP -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source #

ensures_amalgamability :: TPTP -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: TPTP -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: TPTP -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: TPTP -> Symbol -> () Source #

id_to_raw :: TPTP -> Id -> () Source #

matches :: TPTP -> Symbol -> () -> Bool Source #

empty_signature :: TPTP -> Sign Source #

add_symb_to_sign :: TPTP -> Sign -> Symbol -> Result Sign Source #

signature_union :: TPTP -> Sign -> Sign -> Result Sign Source #

signatureDiff :: TPTP -> Sign -> Sign -> Result Sign Source #

intersection :: TPTP -> Sign -> Sign -> Result Sign Source #

final_union :: TPTP -> Sign -> Sign -> Result Sign Source #

morphism_union :: TPTP -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: TPTP -> Sign -> Sign -> Bool Source #

subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism Source #

generated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: TPTP -> EndoMap () -> Sign -> Result Morphism Source #

induced_from_to_morphism :: TPTP -> EndoMap () -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: TPTP -> Morphism -> Bool Source #

is_injective :: TPTP -> Morphism -> Bool Source #

theory_to_taxonomy :: TPTP -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: TPTP -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: TPTP -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: TPTP -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source # 

Methods

parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: TPTP -> Stability Source #

data_logic :: TPTP -> Maybe AnyLogic Source #

top_sublogic :: TPTP -> Sublogic Source #

all_sublogics :: TPTP -> [Sublogic] Source #

bottomSublogic :: TPTP -> Maybe Sublogic Source #

sublogicDimensions :: TPTP -> [[Sublogic]] Source #

parseSublogic :: TPTP -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source #

provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source #

default_prover :: TPTP -> String Source #

cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source #

conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: TPTP -> ProofTree Source #

syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: TPTP -> Maybe OMCD Source #

export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #