Hets - the Heterogeneous Tool Set

Copyright(c) DFKI GmbH Uni Bremen 2002-2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

Common.ProofTree

Description

Datatype for storing of the proof tree

Synopsis

Documentation

data ProofTree Source #

Datatype for storing of the proof tree. The Show class is instantiated.

Constructors

ProofTree String 

Instances

Eq ProofTree Source # 

Methods

(==) :: ProofTree -> ProofTree -> Bool

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

Data ProofTree Source # 

Methods

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

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

toConstr :: ProofTree -> Constr

dataTypeOf :: ProofTree -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ProofTree Source # 

Methods

compare :: ProofTree -> ProofTree -> Ordering

(<) :: ProofTree -> ProofTree -> Bool

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

(>) :: ProofTree -> ProofTree -> Bool

(>=) :: ProofTree -> ProofTree -> Bool

max :: ProofTree -> ProofTree -> ProofTree

min :: ProofTree -> ProofTree -> ProofTree

Show ProofTree Source # 

Methods

showsPrec :: Int -> ProofTree -> ShowS

show :: ProofTree -> String

showList :: [ProofTree] -> ShowS

Logic RDF RDFSub TurtleDocument Axiom SymbItems SymbMapItems Sign RDFMorphism RDFEntity RawSymb ProofTree Source # 

Methods

parse_basic_sen :: RDF -> Maybe (TurtleDocument -> AParser st Axiom) Source #

stability :: RDF -> Stability Source #

data_logic :: RDF -> Maybe AnyLogic Source #

top_sublogic :: RDF -> RDFSub Source #

all_sublogics :: RDF -> [RDFSub] Source #

bottomSublogic :: RDF -> Maybe RDFSub Source #

sublogicDimensions :: RDF -> [[RDFSub]] Source #

parseSublogic :: RDF -> String -> Maybe RDFSub Source #

proj_sublogic_epsilon :: RDF -> RDFSub -> Sign -> RDFMorphism Source #

provers :: RDF -> [Prover Sign Axiom RDFMorphism RDFSub ProofTree] Source #

default_prover :: RDF -> String Source #

cons_checkers :: RDF -> [ConsChecker Sign Axiom RDFSub RDFMorphism ProofTree] Source #

conservativityCheck :: RDF -> [ConservativityChecker Sign Axiom RDFMorphism] Source #

empty_proof_tree :: RDF -> ProofTree Source #

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

omdoc_metatheory :: RDF -> Maybe OMCD Source #

export_symToOmdoc :: RDF -> NameMap RDFEntity -> RDFEntity -> String -> Result TCElement Source #

export_senToOmdoc :: RDF -> NameMap RDFEntity -> Axiom -> Result TCorOMElement Source #

export_theoryToOmdoc :: RDF -> SigMap RDFEntity -> Sign -> [Named Axiom] -> Result [TCElement] Source #

omdocToSym :: RDF -> SigMapI RDFEntity -> TCElement -> String -> Result RDFEntity Source #

omdocToSen :: RDF -> SigMapI RDFEntity -> TCElement -> String -> Result (Maybe (Named Axiom)) Source #

addOMadtToTheory :: RDF -> SigMapI RDFEntity -> (Sign, [Named Axiom]) -> [[OmdADT]] -> Result (Sign, [Named Axiom]) Source #

addOmdocToTheory :: RDF -> SigMapI RDFEntity -> (Sign, [Named Axiom]) -> [TCElement] -> Result (Sign, [Named Axiom]) Source #

Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 

Methods

parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st CASLFORMULA) Source #

stability :: CASL -> Stability Source #

data_logic :: CASL -> Maybe AnyLogic Source #

top_sublogic :: CASL -> CASL_Sublogics Source #

all_sublogics :: CASL -> [CASL_Sublogics] Source #

bottomSublogic :: CASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: CASL -> [[CASL_Sublogics]] Source #

parseSublogic :: CASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: CASL -> CASL_Sublogics -> CASLSign -> CASLMor Source #

provers :: CASL -> [Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree] Source #

default_prover :: CASL -> String Source #

cons_checkers :: CASL -> [ConsChecker CASLSign CASLFORMULA CASL_Sublogics CASLMor ProofTree] Source #

conservativityCheck :: CASL -> [ConservativityChecker CASLSign CASLFORMULA CASLMor] Source #

empty_proof_tree :: CASL -> ProofTree Source #

syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL -> Maybe OMCD Source #

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

export_senToOmdoc :: CASL -> NameMap Symbol -> CASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL -> SigMap Symbol -> CASLSign -> [Named CASLFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: CASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CASLFORMULA)) Source #

addOMadtToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [[OmdADT]] -> Result (CASLSign, [Named CASLFORMULA]) Source #

addOmdocToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [TCElement] -> Result (CASLSign, [Named CASLFORMULA]) Source #

Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source # 

Methods

parse_basic_sen :: CASL_DL -> Maybe (DL_BASIC_SPEC -> AParser st DLFORMULA) Source #

stability :: CASL_DL -> Stability Source #

data_logic :: CASL_DL -> Maybe AnyLogic Source #

top_sublogic :: CASL_DL -> CASL_DL_SL Source #

all_sublogics :: CASL_DL -> [CASL_DL_SL] Source #

bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source #

sublogicDimensions :: CASL_DL -> [[CASL_DL_SL]] Source #

parseSublogic :: CASL_DL -> String -> Maybe CASL_DL_SL Source #

proj_sublogic_epsilon :: CASL_DL -> CASL_DL_SL -> DLSign -> DLMor Source #

provers :: CASL_DL -> [Prover DLSign DLFORMULA DLMor CASL_DL_SL ProofTree] Source #

default_prover :: CASL_DL -> String Source #

cons_checkers :: CASL_DL -> [ConsChecker DLSign DLFORMULA CASL_DL_SL DLMor ProofTree] Source #

conservativityCheck :: CASL_DL -> [ConservativityChecker DLSign DLFORMULA DLMor] Source #

empty_proof_tree :: CASL_DL -> ProofTree Source #

syntaxTable :: CASL_DL -> DLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL_DL -> Maybe OMCD Source #

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

export_senToOmdoc :: CASL_DL -> NameMap Symbol -> DLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL_DL -> SigMap Symbol -> DLSign -> [Named DLFORMULA] -> Result [TCElement] Source #

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

omdocToSen :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named DLFORMULA)) Source #

addOMadtToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [[OmdADT]] -> Result (DLSign, [Named DLFORMULA]) Source #

addOmdocToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [TCElement] -> Result (DLSign, [Named DLFORMULA]) Source #

Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 

Methods

parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source #

stability :: THF -> Stability Source #

data_logic :: THF -> Maybe AnyLogic Source #

top_sublogic :: THF -> THFSl Source #

all_sublogics :: THF -> [THFSl] Source #

bottomSublogic :: THF -> Maybe THFSl Source #

sublogicDimensions :: THF -> [[THFSl]] Source #

parseSublogic :: THF -> String -> Maybe THFSl Source #

proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source #

provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source #

default_prover :: THF -> String Source #

cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source #

conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source #

empty_proof_tree :: THF -> ProofTree Source #

syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source #

omdoc_metatheory :: THF -> Maybe OMCD Source #

export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source #

export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source #

export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source #

omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source #

omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source #

addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source #

addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source #

Logic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 

Methods

parse_basic_sen :: OWL2 -> Maybe (OntologyDocument -> AParser st Axiom) Source #

stability :: OWL2 -> Stability Source #

data_logic :: OWL2 -> Maybe AnyLogic Source #

top_sublogic :: OWL2 -> ProfSub Source #

all_sublogics :: OWL2 -> [ProfSub] Source #

bottomSublogic :: OWL2 -> Maybe ProfSub Source #

sublogicDimensions :: OWL2 -> [[ProfSub]] Source #

parseSublogic :: OWL2 -> String -> Maybe ProfSub Source #

proj_sublogic_epsilon :: OWL2 -> ProfSub -> Sign -> OWLMorphism Source #

provers :: OWL2 -> [Prover Sign Axiom OWLMorphism ProfSub ProofTree] Source #

default_prover :: OWL2 -> String Source #

cons_checkers :: OWL2 -> [ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree] Source #

conservativityCheck :: OWL2 -> [ConservativityChecker Sign Axiom OWLMorphism] Source #

empty_proof_tree :: OWL2 -> ProofTree Source #

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

omdoc_metatheory :: OWL2 -> Maybe OMCD Source #

export_symToOmdoc :: OWL2 -> NameMap Entity -> Entity -> String -> Result TCElement Source #

export_senToOmdoc :: OWL2 -> NameMap Entity -> Axiom -> Result TCorOMElement Source #

export_theoryToOmdoc :: OWL2 -> SigMap Entity -> Sign -> [Named Axiom] -> Result [TCElement] Source #

omdocToSym :: OWL2 -> SigMapI Entity -> TCElement -> String -> Result Entity Source #

omdocToSen :: OWL2 -> SigMapI Entity -> TCElement -> String -> Result (Maybe (Named Axiom)) Source #

addOMadtToTheory :: OWL2 -> SigMapI Entity -> (Sign, [Named Axiom]) -> [[OmdADT]] -> Result (Sign, [Named Axiom]) Source #

addOmdocToTheory :: OWL2 -> SigMapI Entity -> (Sign, [Named Axiom]) -> [TCElement] -> Result (Sign, [Named Axiom]) Source #

Logic Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree Source # 

Methods

parse_basic_sen :: Adl -> Maybe (Context -> AParser st Sen) Source #

stability :: Adl -> Stability Source #

data_logic :: Adl -> Maybe AnyLogic Source #

top_sublogic :: Adl -> () Source #

all_sublogics :: Adl -> [()] Source #

bottomSublogic :: Adl -> Maybe () Source #

sublogicDimensions :: Adl -> [[()]] Source #

parseSublogic :: Adl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Adl -> () -> Sign -> Morphism Source #

provers :: Adl -> [Prover Sign Sen Morphism () ProofTree] Source #

default_prover :: Adl -> String Source #

cons_checkers :: Adl -> [ConsChecker Sign Sen () Morphism ProofTree] Source #

conservativityCheck :: Adl -> [ConservativityChecker Sign Sen Morphism] Source #

empty_proof_tree :: Adl -> ProofTree Source #

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

omdoc_metatheory :: Adl -> Maybe OMCD Source #

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

export_senToOmdoc :: Adl -> NameMap Symbol -> Sen -> Result TCorOMElement Source #

export_theoryToOmdoc :: Adl -> SigMap Symbol -> Sign -> [Named Sen] -> Result [TCElement] Source #

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

omdocToSen :: Adl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sen)) Source #

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

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

Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

parse_basic_sen :: CommonLogic -> Maybe (BASIC_SPEC -> AParser st TEXT_META) Source #

stability :: CommonLogic -> Stability Source #

data_logic :: CommonLogic -> Maybe AnyLogic Source #

top_sublogic :: CommonLogic -> CommonLogicSL Source #

all_sublogics :: CommonLogic -> [CommonLogicSL] Source #

bottomSublogic :: CommonLogic -> Maybe CommonLogicSL Source #

sublogicDimensions :: CommonLogic -> [[CommonLogicSL]] Source #

parseSublogic :: CommonLogic -> String -> Maybe CommonLogicSL Source #

proj_sublogic_epsilon :: CommonLogic -> CommonLogicSL -> Sign -> Morphism Source #

provers :: CommonLogic -> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree] Source #

default_prover :: CommonLogic -> String Source #

cons_checkers :: CommonLogic -> [ConsChecker Sign TEXT_META CommonLogicSL Morphism ProofTree] Source #

conservativityCheck :: CommonLogic -> [ConservativityChecker Sign TEXT_META Morphism] Source #

empty_proof_tree :: CommonLogic -> ProofTree Source #

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

omdoc_metatheory :: CommonLogic -> Maybe OMCD Source #

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

export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement Source #

export_theoryToOmdoc :: CommonLogic -> SigMap Symbol -> Sign -> [Named TEXT_META] -> Result [TCElement] Source #

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

omdocToSen :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named TEXT_META)) Source #

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

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

Logic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #

Instance of Logic for propositional logc

Methods

parse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #

stability :: Propositional -> Stability Source #

data_logic :: Propositional -> Maybe AnyLogic Source #

top_sublogic :: Propositional -> PropSL Source #

all_sublogics :: Propositional -> [PropSL] Source #

bottomSublogic :: Propositional -> Maybe PropSL Source #

sublogicDimensions :: Propositional -> [[PropSL]] Source #

parseSublogic :: Propositional -> String -> Maybe PropSL Source #

proj_sublogic_epsilon :: Propositional -> PropSL -> Sign -> Morphism Source #

provers :: Propositional -> [Prover Sign FORMULA Morphism PropSL ProofTree] Source #

default_prover :: Propositional -> String Source #

cons_checkers :: Propositional -> [ConsChecker Sign FORMULA PropSL Morphism ProofTree] Source #

conservativityCheck :: Propositional -> [ConservativityChecker Sign FORMULA Morphism] Source #

empty_proof_tree :: Propositional -> ProofTree Source #

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

omdoc_metatheory :: Propositional -> Maybe OMCD Source #

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

export_senToOmdoc :: Propositional -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Propositional -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source #

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

omdocToSen :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #

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

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

Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #

Instance of Logic for propositional logc

Methods

parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source #

stability :: QBF -> Stability Source #

data_logic :: QBF -> Maybe AnyLogic Source #

top_sublogic :: QBF -> QBFSL Source #

all_sublogics :: QBF -> [QBFSL] Source #

bottomSublogic :: QBF -> Maybe QBFSL Source #

sublogicDimensions :: QBF -> [[QBFSL]] Source #

parseSublogic :: QBF -> String -> Maybe QBFSL Source #

proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source #

provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source #

default_prover :: QBF -> String Source #

cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source #

conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source #

empty_proof_tree :: QBF -> ProofTree Source #

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

omdoc_metatheory :: QBF -> Maybe OMCD Source #

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

export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source #

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

omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #

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

addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) 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 #

Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source #

sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source #

sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source #

minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source #

targetLogic :: CommonLogicModuleElimination -> CommonLogic Source #

mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source #

map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source #

map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source #

map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source #

extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source #

is_model_transportable :: CommonLogicModuleElimination -> Bool Source #

has_model_expansion :: CommonLogicModuleElimination -> Bool Source #

is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source #

constituents :: CommonLogicModuleElimination -> [String] Source #

isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source #

rps :: CommonLogicModuleElimination -> Bool Source #

eps :: CommonLogicModuleElimination -> Bool Source #

Comorphism OWL22CommonLogic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism Prop2CommonLogic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism Propositional2OWL2 Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism DMU2OWL2 DMU () Text () () () Text (DefaultMorphism Text) () () () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 

Methods

parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source #

stability :: SoftFOL -> Stability Source #

data_logic :: SoftFOL -> Maybe AnyLogic Source #

top_sublogic :: SoftFOL -> () Source #

all_sublogics :: SoftFOL -> [()] Source #

bottomSublogic :: SoftFOL -> Maybe () Source #

sublogicDimensions :: SoftFOL -> [[()]] Source #

parseSublogic :: SoftFOL -> String -> Maybe () Source #

proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source #

provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source #

default_prover :: SoftFOL -> String Source #

cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source #

conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source #

empty_proof_tree :: SoftFOL -> ProofTree Source #

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

omdoc_metatheory :: SoftFOL -> Maybe OMCD Source #

export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source #

omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

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

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

Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #