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
Safe Haskell	None

TPTP.Sublogic

Description

Data structures representing TPTP sublogics.

Documentation

data Sublogic Source #

Constructors

CNF
FOF
TFF
THF

Instances

Instances details

Eq Sublogic Source #
Instance details Defined in TPTP.Sublogic Methods (==) :: Sublogic -> Sublogic -> Bool (/=) :: Sublogic -> Sublogic -> Bool
Data Sublogic Source #
Instance details Defined in TPTP.Sublogic 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 :: forall r r'. (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 #
Instance details Defined in TPTP.Sublogic 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 #
Instance details Defined in TPTP.Sublogic Methods showsPrec :: Int -> Sublogic -> ShowS show :: Sublogic -> String showList :: [Sublogic] -> ShowS
Generic Sublogic
Instance details Defined in TPTP.ATC_TPTP Associated Types type Rep Sublogic :: Type -> Type Methods from :: Sublogic -> Rep Sublogic x to :: Rep Sublogic x -> Sublogic
FromJSON Sublogic
Instance details Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser Sublogic parseJSONList :: Value -> Parser [Sublogic]
ToJSON Sublogic
Instance details Defined in TPTP.ATC_TPTP Methods toJSON :: Sublogic -> Value toEncoding :: Sublogic -> Encoding toJSONList :: [Sublogic] -> Value toEncodingList :: [Sublogic] -> Encoding
ShATermConvertible Sublogic
Instance details Defined in TPTP.ATC_TPTP Methods toShATermAux :: ATermTable -> Sublogic -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sublogic] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sublogic) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sublogic])
SublogicName Sublogic Source #
Instance details Defined in TPTP.Logic_TPTP Methods sublogicName :: Sublogic -> String Source #
SemiLatticeWithTop Sublogic Source #
Instance details Defined in TPTP.Logic_TPTP Methods lub :: Sublogic -> Sublogic -> Sublogic Source # top :: Sublogic Source #
ProjectSublogicM Sublogic () Source #
Instance details Defined in TPTP.Logic_TPTP Methods projectSublogicM :: Sublogic -> () -> Maybe () Source #
ProjectSublogicM Sublogic Symbol Source #
Instance details Defined in TPTP.Logic_TPTP Methods projectSublogicM :: Sublogic -> Symbol -> Maybe Symbol Source #
ProjectSublogic Sublogic BASIC_SPEC Source #
Instance details Defined in TPTP.Logic_TPTP Methods projectSublogic :: Sublogic -> BASIC_SPEC -> BASIC_SPEC Source #
ProjectSublogic Sublogic Sign Source #
Instance details Defined in TPTP.Logic_TPTP Methods projectSublogic :: Sublogic -> Sign -> Sign Source #
ProjectSublogic Sublogic Sentence Source #
Instance details Defined in TPTP.Logic_TPTP Methods projectSublogic :: Sublogic -> Sentence -> Sentence Source #
ProjectSublogic Sublogic Morphism Source #
Instance details Defined in TPTP.Logic_TPTP Methods projectSublogic :: Sublogic -> Morphism -> Morphism Source #
MinSublogic Sublogic () Source #
Instance details Defined in TPTP.Logic_TPTP Methods minSublogic :: () -> Sublogic Source #
MinSublogic Sublogic BASIC_SPEC Source #
Instance details Defined in TPTP.Logic_TPTP Methods minSublogic :: BASIC_SPEC -> Sublogic Source #
MinSublogic Sublogic Sign Source #
Instance details Defined in TPTP.Logic_TPTP Methods minSublogic :: Sign -> Sublogic Source #
MinSublogic Sublogic Symbol Source #
Instance details Defined in TPTP.Logic_TPTP Methods minSublogic :: Symbol -> Sublogic Source #
MinSublogic Sublogic Sentence Source #
Instance details Defined in TPTP.Logic_TPTP Methods minSublogic :: Sentence -> Sublogic Source #
MinSublogic Sublogic Morphism Source #
Instance details Defined in TPTP.Logic_TPTP Methods minSublogic :: Morphism -> Sublogic Source #
Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source #
Instance details Defined in TPTP.Logic_TPTP 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 # sublogicOfTheo :: TPTP -> (Sign, [Sentence]) -> Sublogic Source #
type Rep Sublogic
Instance details Defined in TPTP.ATC_TPTP type Rep Sublogic = D1 ('MetaData "Sublogic" "TPTP.Sublogic" "main" 'False) ((C1 ('MetaCons "CNF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FOF" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TFF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "THF" 'PrefixI 'False) (U1 :: Type -> Type)))

top :: Sublogic Source #

bottom :: Sublogic Source #

sublogicName :: Sublogic -> String Source #

leastUpperBound :: Sublogic -> Sublogic -> Sublogic Source #

sublogicOfUnit :: Sublogic -> () -> Sublogic Source #

sublogicOfBaiscSpec :: Sublogic -> BASIC_SPEC -> Sublogic Source #

sublogicOfSentence :: Sublogic -> Sentence -> Sublogic Source #

sublogicOfSymbol :: Sublogic -> Symbol -> Sublogic Source #

sublogicOfSign :: Sublogic -> Sign -> Sublogic Source #

sublogicOfMorphism :: Sublogic -> Morphism -> Sublogic Source #

projectSublogicBasicSpec :: Sublogic -> BASIC_SPEC -> BASIC_SPEC Source #

projectSublogicSign :: Sublogic -> Sign -> Sign Source #

projectSublogicSentence :: Sublogic -> Sentence -> Sentence Source #

projectSublogicMorphism :: Sublogic -> Morphism -> Morphism Source #

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

projectSublogicMSymbol :: Sublogic -> Symbol -> Maybe Symbol Source #