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
Safe HaskellNone

TPTP.Sublogic

Description

Data structures representing TPTP sublogics.

Documentation

data Sublogic Source #

Constructors

CNF 
FOF 
TFF 
THF 

Instances

Eq Sublogic Source # 

Methods

(==) :: Sublogic -> Sublogic -> Bool

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

Data Sublogic Source # 

Methods

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

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

toConstr :: Sublogic -> Constr

dataTypeOf :: Sublogic -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Sublogic Source # 

Methods

compare :: Sublogic -> Sublogic -> Ordering

(<) :: Sublogic -> Sublogic -> Bool

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

(>) :: Sublogic -> Sublogic -> Bool

(>=) :: Sublogic -> Sublogic -> Bool

max :: Sublogic -> Sublogic -> Sublogic

min :: Sublogic -> Sublogic -> Sublogic

Show Sublogic Source # 

Methods

showsPrec :: Int -> Sublogic -> ShowS

show :: Sublogic -> String

showList :: [Sublogic] -> ShowS

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 #

projectSublogicMUnit :: Sublogic -> () -> Maybe () Source #