Hets - the Heterogeneous Tool Set
Copyright(c) DFKI GmbH Uni Bremen 2002-2008 Tom Kranz 2021-2022
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (via DeriveDataTypeable, FlexibleInstances)
Safe HaskellNone

Common.ProofTree

Description

Datatype for storing of the proof tree. Actual proof tree (dag) structures can be printed as dot (Graphviz) digraphs.

Documentation

data ProofTree Source #

Constructors

ProofTree String 
ProofGraph (Gr ProofGraphNode Int) 

Instances

Instances details
Eq ProofTree Source # 
Instance details

Defined in Common.ProofTree

Methods

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

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

Ord ProofTree Source # 
Instance details

Defined in Common.ProofTree

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 # 
Instance details

Defined in Common.ProofTree

Methods

showsPrec :: Int -> ProofTree -> ShowS

show :: ProofTree -> String

showList :: [ProofTree] -> ShowS

Generic ProofTree 
Instance details

Defined in ATC.ProofTree

Associated Types

type Rep ProofTree :: Type -> Type

Methods

from :: ProofTree -> Rep ProofTree x

to :: Rep ProofTree x -> ProofTree

FromJSON ProofTree 
Instance details

Defined in ATC.ProofTree

Methods

parseJSON :: Value -> Parser ProofTree

parseJSONList :: Value -> Parser [ProofTree]

ToJSON ProofTree 
Instance details

Defined in ATC.ProofTree

Methods

toJSON :: ProofTree -> Value

toEncoding :: ProofTree -> Encoding

toJSONList :: [ProofTree] -> Value

toEncodingList :: [ProofTree] -> Encoding

ShATermConvertible ProofTree 
Instance details

Defined in ATC.ProofTree

Methods

toShATermAux :: ATermTable -> ProofTree -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ProofTree] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofTree)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofTree])

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

Defined in RDF.Logic_RDF

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 #

sublogicOfTheo :: RDF -> (Sign, [Axiom]) -> RDFSub Source #

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

Defined in THF.Logic_THF

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 #

sublogicOfTheo :: THF -> (SignTHF, [THFFormula]) -> THFSl 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 #

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

Instance of Logic for propositional logc

Instance details

Defined in QBF.Logic_QBF

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 #

sublogicOfTheo :: QBF -> (Sign, [FORMULA]) -> QBFSL Source #

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

Instance of Logic for propositional logc

Instance details

Defined in Propositional.Logic_Propositional

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 #

sublogicOfTheo :: Propositional -> (Sign, [FORMULA]) -> PropSL Source #

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

Defined in OWL2.Logic_OWL2

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 #

sublogicOfTheo :: OWL2 -> (Sign, [Axiom]) -> ProfSub Source #

Logic NeSyPatterns () BASIC_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #

Instance of Logic for propositional logc

Instance details

Defined in NeSyPatterns.Logic_NeSyPatterns

Methods

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

stability :: NeSyPatterns -> Stability Source #

data_logic :: NeSyPatterns -> Maybe AnyLogic Source #

top_sublogic :: NeSyPatterns -> () Source #

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

bottomSublogic :: NeSyPatterns -> Maybe () Source #

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

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

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

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

default_prover :: NeSyPatterns -> String Source #

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

conservativityCheck :: NeSyPatterns -> [ConservativityChecker Sign () Morphism] Source #

empty_proof_tree :: NeSyPatterns -> ProofTree Source #

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

omdoc_metatheory :: NeSyPatterns -> Maybe OMCD Source #

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

export_senToOmdoc :: NeSyPatterns -> NameMap Symbol -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: NeSyPatterns -> SigMap Symbol -> Sign -> [Named ()] -> Result [TCElement] Source #

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

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

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

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

sublogicOfTheo :: NeSyPatterns -> (Sign, [()]) -> () Source #

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

Defined in CommonLogic.Logic_CommonLogic

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 #

sublogicOfTheo :: CommonLogic -> (Sign, [TEXT_META]) -> CommonLogicSL Source #

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

Defined in Adl.Logic_Adl

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 #

sublogicOfTheo :: Adl -> (Sign, [Sen]) -> () Source #

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

Defined in CASL.Logic_CASL

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 #

sublogicOfTheo :: CASL -> (CASLSign, [CASLFORMULA]) -> CASL_Sublogics Source #

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

Defined in CASL_DL.Logic_CASL_DL

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 #

sublogicOfTheo :: CASL_DL -> (DLSign, [DLFORMULA]) -> CASL_DL_SL 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 # 
Instance details

Defined in OWL2.Propositional2OWL2

Methods

sourceLogic :: Propositional2OWL2 -> Propositional Source #

sourceSublogic :: Propositional2OWL2 -> PropSL Source #

sourceSublogicLossy :: Propositional2OWL2 -> PropSL Source #

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

targetLogic :: Propositional2OWL2 -> OWL2 Source #

mapSublogic :: Propositional2OWL2 -> PropSL -> Maybe ProfSub Source #

map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #

mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #

map_morphism :: Propositional2OWL2 -> Morphism -> Result OWLMorphism Source #

map_sentence :: Propositional2OWL2 -> Sign -> FORMULA -> Result Axiom Source #

map_symbol :: Propositional2OWL2 -> Sign -> Symbol -> Set Entity Source #

extractModel :: Propositional2OWL2 -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source #

is_model_transportable :: Propositional2OWL2 -> Bool Source #

has_model_expansion :: Propositional2OWL2 -> Bool Source #

is_weakly_amalgamable :: Propositional2OWL2 -> Bool Source #

constituents :: Propositional2OWL2 -> [String] Source #

isInclusionComorphism :: Propositional2OWL2 -> Bool Source #

rps :: Propositional2OWL2 -> Bool Source #

eps :: Propositional2OWL2 -> Bool Source #

isGTC :: Propositional2OWL2 -> Bool Source #

Comorphism OWL22NeSyPatterns OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree NeSyPatterns () BASIC_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Instance details

Defined in OWL2.OWL22NeSyPatterns

Methods

sourceLogic :: OWL22NeSyPatterns -> OWL2 Source #

sourceSublogic :: OWL22NeSyPatterns -> ProfSub Source #

sourceSublogicLossy :: OWL22NeSyPatterns -> ProfSub Source #

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

targetLogic :: OWL22NeSyPatterns -> NeSyPatterns Source #

mapSublogic :: OWL22NeSyPatterns -> ProfSub -> Maybe () Source #

map_theory :: OWL22NeSyPatterns -> (Sign0, [Named Axiom]) -> Result (Sign, [Named ()]) Source #

mapMarkedTheory :: OWL22NeSyPatterns -> (Sign0, [Named Axiom]) -> Result (Sign, [Named ()]) Source #

map_morphism :: OWL22NeSyPatterns -> OWLMorphism -> Result Morphism Source #

map_sentence :: OWL22NeSyPatterns -> Sign0 -> Axiom -> Result () Source #

map_symbol :: OWL22NeSyPatterns -> Sign0 -> Entity -> Set Symbol Source #

extractModel :: OWL22NeSyPatterns -> Sign0 -> ProofTree -> Result (Sign0, [Named Axiom]) Source #

is_model_transportable :: OWL22NeSyPatterns -> Bool Source #

has_model_expansion :: OWL22NeSyPatterns -> Bool Source #

is_weakly_amalgamable :: OWL22NeSyPatterns -> Bool Source #

constituents :: OWL22NeSyPatterns -> [String] Source #

isInclusionComorphism :: OWL22NeSyPatterns -> Bool Source #

rps :: OWL22NeSyPatterns -> Bool Source #

eps :: OWL22NeSyPatterns -> Bool Source #

isGTC :: OWL22NeSyPatterns -> Bool Source #

Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Instance details

Defined in Comorphisms.THFP_P2THFP

Methods

sourceLogic :: THFP_P2THFP -> THF Source #

sourceSublogic :: THFP_P2THFP -> THFSl Source #

sourceSublogicLossy :: THFP_P2THFP -> THFSl Source #

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

targetLogic :: THFP_P2THFP -> THF Source #

mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source #

map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source #

map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source #

map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source #

extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source #

is_model_transportable :: THFP_P2THFP -> Bool Source #

has_model_expansion :: THFP_P2THFP -> Bool Source #

is_weakly_amalgamable :: THFP_P2THFP -> Bool Source #

constituents :: THFP_P2THFP -> [String] Source #

isInclusionComorphism :: THFP_P2THFP -> Bool Source #

rps :: THFP_P2THFP -> Bool Source #

eps :: THFP_P2THFP -> Bool Source #

isGTC :: THFP_P2THFP -> Bool Source #

Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.THFP_P2HasCASL

Methods

sourceLogic :: THFP_P2HasCASL -> THF Source #

sourceSublogic :: THFP_P2HasCASL -> THFSl Source #

sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source #

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

targetLogic :: THFP_P2HasCASL -> HasCASL Source #

mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source #

map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source #

mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source #

map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source #

map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source #

map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source #

extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source #

is_model_transportable :: THFP_P2HasCASL -> Bool Source #

has_model_expansion :: THFP_P2HasCASL -> Bool Source #

is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source #

constituents :: THFP_P2HasCASL -> [String] Source #

isInclusionComorphism :: THFP_P2HasCASL -> Bool Source #

rps :: THFP_P2HasCASL -> Bool Source #

eps :: THFP_P2HasCASL -> Bool Source #

isGTC :: THFP_P2HasCASL -> Bool Source #

Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Instance details

Defined in Comorphisms.THFP2THF0

Methods

sourceLogic :: THFP2THF0 -> THF Source #

sourceSublogic :: THFP2THF0 -> THFSl Source #

sourceSublogicLossy :: THFP2THF0 -> THFSl Source #

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

targetLogic :: THFP2THF0 -> THF Source #

mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source #

map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source #

map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source #

map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source #

extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source #

is_model_transportable :: THFP2THF0 -> Bool Source #

has_model_expansion :: THFP2THF0 -> Bool Source #

is_weakly_amalgamable :: THFP2THF0 -> Bool Source #

constituents :: THFP2THF0 -> [String] Source #

isInclusionComorphism :: THFP2THF0 -> Bool Source #

rps :: THFP2THF0 -> Bool Source #

eps :: THFP2THF0 -> Bool Source #

isGTC :: THFP2THF0 -> Bool 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 # 
Instance details

Defined in Comorphisms.QBF2Prop

Methods

sourceLogic :: QBF2Prop -> QBF Source #

sourceSublogic :: QBF2Prop -> QBFSL Source #

sourceSublogicLossy :: QBF2Prop -> QBFSL Source #

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

targetLogic :: QBF2Prop -> Propositional Source #

mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL Source #

map_theory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #

mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #

map_morphism :: QBF2Prop -> Morphism -> Result Morphism0 Source #

map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA0 Source #

map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: QBF2Prop -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source #

is_model_transportable :: QBF2Prop -> Bool Source #

has_model_expansion :: QBF2Prop -> Bool Source #

is_weakly_amalgamable :: QBF2Prop -> Bool Source #

constituents :: QBF2Prop -> [String] Source #

isInclusionComorphism :: QBF2Prop -> Bool Source #

rps :: QBF2Prop -> Bool Source #

eps :: QBF2Prop -> Bool Source #

isGTC :: QBF2Prop -> Bool 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 # 
Instance details

Defined in Comorphisms.Prop2QBF

Methods

sourceLogic :: Prop2QBF -> Propositional Source #

sourceSublogic :: Prop2QBF -> PropSL Source #

sourceSublogicLossy :: Prop2QBF -> PropSL Source #

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

targetLogic :: Prop2QBF -> QBF Source #

mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL Source #

map_theory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #

mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #

map_morphism :: Prop2QBF -> Morphism0 -> Result Morphism Source #

map_sentence :: Prop2QBF -> Sign -> FORMULA0 -> Result FORMULA Source #

map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source #

extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA0]) Source #

is_model_transportable :: Prop2QBF -> Bool Source #

has_model_expansion :: Prop2QBF -> Bool Source #

is_weakly_amalgamable :: Prop2QBF -> Bool Source #

constituents :: Prop2QBF -> [String] Source #

isInclusionComorphism :: Prop2QBF -> Bool Source #

rps :: Prop2QBF -> Bool Source #

eps :: Prop2QBF -> Bool Source #

isGTC :: Prop2QBF -> Bool Source #

Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Instance details

Defined in Comorphisms.HasCASL2THFP_P

Methods

sourceLogic :: HasCASL2THFP_P -> HasCASL Source #

sourceSublogic :: HasCASL2THFP_P -> Sublogic Source #

sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source #

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

targetLogic :: HasCASL2THFP_P -> THF Source #

mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source #

map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source #

mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source #

map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source #

map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source #

map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source #

extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source #

is_model_transportable :: HasCASL2THFP_P -> Bool Source #

has_model_expansion :: HasCASL2THFP_P -> Bool Source #

is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source #

constituents :: HasCASL2THFP_P -> [String] Source #

isInclusionComorphism :: HasCASL2THFP_P -> Bool Source #

rps :: HasCASL2THFP_P -> Bool Source #

eps :: HasCASL2THFP_P -> Bool Source #

isGTC :: HasCASL2THFP_P -> 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 # 
Instance details

Defined in OWL2.OWL22CommonLogic

Methods

sourceLogic :: OWL22CommonLogic -> OWL2 Source #

sourceSublogic :: OWL22CommonLogic -> ProfSub Source #

sourceSublogicLossy :: OWL22CommonLogic -> ProfSub Source #

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

targetLogic :: OWL22CommonLogic -> CommonLogic Source #

mapSublogic :: OWL22CommonLogic -> ProfSub -> Maybe CommonLogicSL Source #

map_theory :: OWL22CommonLogic -> (Sign, [Named Axiom]) -> Result (Sign0, [Named TEXT_META]) Source #

mapMarkedTheory :: OWL22CommonLogic -> (Sign, [Named Axiom]) -> Result (Sign0, [Named TEXT_META]) Source #

map_morphism :: OWL22CommonLogic -> OWLMorphism -> Result Morphism Source #

map_sentence :: OWL22CommonLogic -> Sign -> Axiom -> Result TEXT_META Source #

map_symbol :: OWL22CommonLogic -> Sign -> Entity -> Set Symbol Source #

extractModel :: OWL22CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source #

is_model_transportable :: OWL22CommonLogic -> Bool Source #

has_model_expansion :: OWL22CommonLogic -> Bool Source #

is_weakly_amalgamable :: OWL22CommonLogic -> Bool Source #

constituents :: OWL22CommonLogic -> [String] Source #

isInclusionComorphism :: OWL22CommonLogic -> Bool Source #

rps :: OWL22CommonLogic -> Bool Source #

eps :: OWL22CommonLogic -> Bool Source #

isGTC :: OWL22CommonLogic -> Bool 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 # 
Instance details

Defined in Comorphisms.Prop2CommonLogic

Methods

sourceLogic :: Prop2CommonLogic -> Propositional Source #

sourceSublogic :: Prop2CommonLogic -> PropSL Source #

sourceSublogicLossy :: Prop2CommonLogic -> PropSL Source #

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

targetLogic :: Prop2CommonLogic -> CommonLogic Source #

mapSublogic :: Prop2CommonLogic -> PropSL -> Maybe CommonLogicSL Source #

map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #

mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #

map_morphism :: Prop2CommonLogic -> Morphism -> Result Morphism0 Source #

map_sentence :: Prop2CommonLogic -> Sign -> FORMULA -> Result TEXT_META Source #

map_symbol :: Prop2CommonLogic -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: Prop2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source #

is_model_transportable :: Prop2CommonLogic -> Bool Source #

has_model_expansion :: Prop2CommonLogic -> Bool Source #

is_weakly_amalgamable :: Prop2CommonLogic -> Bool Source #

constituents :: Prop2CommonLogic -> [String] Source #

isInclusionComorphism :: Prop2CommonLogic -> Bool Source #

rps :: Prop2CommonLogic -> Bool Source #

eps :: Prop2CommonLogic -> Bool Source #

isGTC :: Prop2CommonLogic -> Bool 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 # 
Instance details

Defined in Comorphisms.CommonLogicModuleElimination

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 #

isGTC :: CommonLogicModuleElimination -> Bool Source #

Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CommonLogic2IsabelleHOL

Methods

sourceLogic :: CommonLogic2IsabelleHOL -> CommonLogic Source #

sourceSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL Source #

sourceSublogicLossy :: CommonLogic2IsabelleHOL -> CommonLogicSL Source #

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

targetLogic :: CommonLogic2IsabelleHOL -> Isabelle Source #

mapSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL -> Maybe () Source #

map_theory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: CommonLogic2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source #

map_sentence :: CommonLogic2IsabelleHOL -> Sign0 -> TEXT_META -> Result Sentence Source #

map_symbol :: CommonLogic2IsabelleHOL -> Sign0 -> Symbol -> Set () Source #

extractModel :: CommonLogic2IsabelleHOL -> Sign0 -> () -> Result (Sign0, [Named TEXT_META]) Source #

is_model_transportable :: CommonLogic2IsabelleHOL -> Bool Source #

has_model_expansion :: CommonLogic2IsabelleHOL -> Bool Source #

is_weakly_amalgamable :: CommonLogic2IsabelleHOL -> Bool Source #

constituents :: CommonLogic2IsabelleHOL -> [String] Source #

isInclusionComorphism :: CommonLogic2IsabelleHOL -> Bool Source #

rps :: CommonLogic2IsabelleHOL -> Bool Source #

eps :: CommonLogic2IsabelleHOL -> Bool Source #

isGTC :: CommonLogic2IsabelleHOL -> Bool 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 # 
Instance details

Defined in OWL2.OWL22CASL

Methods

sourceLogic :: OWL22CASL -> OWL2 Source #

sourceSublogic :: OWL22CASL -> ProfSub Source #

sourceSublogicLossy :: OWL22CASL -> ProfSub Source #

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

targetLogic :: OWL22CASL -> CASL Source #

mapSublogic :: OWL22CASL -> ProfSub -> Maybe CASL_Sublogics Source #

map_theory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: OWL22CASL -> (Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: OWL22CASL -> OWLMorphism -> Result CASLMor Source #

map_sentence :: OWL22CASL -> Sign -> Axiom -> Result CASLFORMULA Source #

map_symbol :: OWL22CASL -> Sign -> Entity -> Set Symbol Source #

extractModel :: OWL22CASL -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source #

is_model_transportable :: OWL22CASL -> Bool Source #

has_model_expansion :: OWL22CASL -> Bool Source #

is_weakly_amalgamable :: OWL22CASL -> Bool Source #

constituents :: OWL22CASL -> [String] Source #

isInclusionComorphism :: OWL22CASL -> Bool Source #

rps :: OWL22CASL -> Bool Source #

eps :: OWL22CASL -> Bool Source #

isGTC :: OWL22CASL -> Bool 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 # 
Instance details

Defined in OWL2.CASL2OWL

Methods

sourceLogic :: CASL2OWL -> CASL Source #

sourceSublogic :: CASL2OWL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2OWL -> CASL_Sublogics Source #

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

targetLogic :: CASL2OWL -> OWL2 Source #

mapSublogic :: CASL2OWL -> CASL_Sublogics -> Maybe ProfSub Source #

map_theory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source #

mapMarkedTheory :: CASL2OWL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Axiom]) Source #

map_morphism :: CASL2OWL -> CASLMor -> Result OWLMorphism Source #

map_sentence :: CASL2OWL -> CASLSign -> CASLFORMULA -> Result Axiom Source #

map_symbol :: CASL2OWL -> CASLSign -> Symbol -> Set Entity Source #

extractModel :: CASL2OWL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2OWL -> Bool Source #

has_model_expansion :: CASL2OWL -> Bool Source #

is_weakly_amalgamable :: CASL2OWL -> Bool Source #

constituents :: CASL2OWL -> [String] Source #

isInclusionComorphism :: CASL2OWL -> Bool Source #

rps :: CASL2OWL -> Bool Source #

eps :: CASL2OWL -> Bool Source #

isGTC :: CASL2OWL -> Bool 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 # 
Instance details

Defined in Comorphisms.ExtModal2OWL

Methods

sourceLogic :: ExtModal2OWL -> ExtModal Source #

sourceSublogic :: ExtModal2OWL -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2OWL -> ExtModalSL Source #

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

targetLogic :: ExtModal2OWL -> OWL2 Source #

mapSublogic :: ExtModal2OWL -> ExtModalSL -> Maybe ProfSub Source #

map_theory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source #

mapMarkedTheory :: ExtModal2OWL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Sign, [Named Axiom]) Source #

map_morphism :: ExtModal2OWL -> ExtModalMorph -> Result OWLMorphism Source #

map_sentence :: ExtModal2OWL -> ExtModalSign -> ExtModalFORMULA -> Result Axiom Source #

map_symbol :: ExtModal2OWL -> ExtModalSign -> Symbol -> Set Entity Source #

extractModel :: ExtModal2OWL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

is_model_transportable :: ExtModal2OWL -> Bool Source #

has_model_expansion :: ExtModal2OWL -> Bool Source #

is_weakly_amalgamable :: ExtModal2OWL -> Bool Source #

constituents :: ExtModal2OWL -> [String] Source #

isInclusionComorphism :: ExtModal2OWL -> Bool Source #

rps :: ExtModal2OWL -> Bool Source #

eps :: ExtModal2OWL -> Bool Source #

isGTC :: ExtModal2OWL -> Bool 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 # 
Instance details

Defined in Comorphisms.RelScheme2CASL

Methods

sourceLogic :: RelScheme2CASL -> RelScheme Source #

sourceSublogic :: RelScheme2CASL -> () Source #

sourceSublogicLossy :: RelScheme2CASL -> () Source #

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

targetLogic :: RelScheme2CASL -> CASL Source #

mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: RelScheme2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor Source #

map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA Source #

map_symbol :: RelScheme2CASL -> Sign -> RSSymbol -> Set Symbol Source #

extractModel :: RelScheme2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source #

is_model_transportable :: RelScheme2CASL -> Bool Source #

has_model_expansion :: RelScheme2CASL -> Bool Source #

is_weakly_amalgamable :: RelScheme2CASL -> Bool Source #

constituents :: RelScheme2CASL -> [String] Source #

isInclusionComorphism :: RelScheme2CASL -> Bool Source #

rps :: RelScheme2CASL -> Bool Source #

eps :: RelScheme2CASL -> Bool Source #

isGTC :: RelScheme2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.Prop2CASL

Methods

sourceLogic :: Prop2CASL -> Propositional Source #

sourceSublogic :: Prop2CASL -> PropSL Source #

sourceSublogicLossy :: Prop2CASL -> PropSL Source #

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

targetLogic :: Prop2CASL -> CASL Source #

mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source #

map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Prop2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: Prop2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source #

map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: Prop2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source #

is_model_transportable :: Prop2CASL -> Bool Source #

has_model_expansion :: Prop2CASL -> Bool Source #

is_weakly_amalgamable :: Prop2CASL -> Bool Source #

constituents :: Prop2CASL -> [String] Source #

isInclusionComorphism :: Prop2CASL -> Bool Source #

rps :: Prop2CASL -> Bool Source #

eps :: Prop2CASL -> Bool Source #

isGTC :: Prop2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.Modal2CASL

Methods

sourceLogic :: Modal2CASL -> Modal Source #

sourceSublogic :: Modal2CASL -> () Source #

sourceSublogicLossy :: Modal2CASL -> () Source #

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

targetLogic :: Modal2CASL -> CASL Source #

mapSublogic :: Modal2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Modal2CASL -> (MSign, [Named ModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Modal2CASL -> ModalMor -> Result CASLMor Source #

map_sentence :: Modal2CASL -> MSign -> ModalFORMULA -> Result CASLFORMULA Source #

map_symbol :: Modal2CASL -> MSign -> Symbol -> Set Symbol Source #

extractModel :: Modal2CASL -> MSign -> ProofTree -> Result (MSign, [Named ModalFORMULA]) Source #

is_model_transportable :: Modal2CASL -> Bool Source #

has_model_expansion :: Modal2CASL -> Bool Source #

is_weakly_amalgamable :: Modal2CASL -> Bool Source #

constituents :: Modal2CASL -> [String] Source #

isInclusionComorphism :: Modal2CASL -> Bool Source #

rps :: Modal2CASL -> Bool Source #

eps :: Modal2CASL -> Bool Source #

isGTC :: Modal2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.Maude2CASL

Methods

sourceLogic :: Maude2CASL -> Maude Source #

sourceSublogic :: Maude2CASL -> () Source #

sourceSublogicLossy :: Maude2CASL -> () Source #

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

targetLogic :: Maude2CASL -> CASL Source #

mapSublogic :: Maude2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Maude2CASL -> (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Maude2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: Maude2CASL -> Sign -> Sentence -> Result CASLFORMULA Source #

map_symbol :: Maude2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: Maude2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source #

is_model_transportable :: Maude2CASL -> Bool Source #

has_model_expansion :: Maude2CASL -> Bool Source #

is_weakly_amalgamable :: Maude2CASL -> Bool Source #

constituents :: Maude2CASL -> [String] Source #

isInclusionComorphism :: Maude2CASL -> Bool Source #

rps :: Maude2CASL -> Bool Source #

eps :: Maude2CASL -> Bool Source #

isGTC :: Maude2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.ExtModal2CASL

Methods

sourceLogic :: ExtModal2CASL -> ExtModal Source #

sourceSublogic :: ExtModal2CASL -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2CASL -> ExtModalSL Source #

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

targetLogic :: ExtModal2CASL -> CASL Source #

mapSublogic :: ExtModal2CASL -> ExtModalSL -> Maybe CASL_Sublogics Source #

map_theory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: ExtModal2CASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: ExtModal2CASL -> ExtModalMorph -> Result CASLMor Source #

map_sentence :: ExtModal2CASL -> ExtModalSign -> ExtModalFORMULA -> Result CASLFORMULA Source #

map_symbol :: ExtModal2CASL -> ExtModalSign -> Symbol -> Set Symbol Source #

extractModel :: ExtModal2CASL -> ExtModalSign -> ProofTree -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

is_model_transportable :: ExtModal2CASL -> Bool Source #

has_model_expansion :: ExtModal2CASL -> Bool Source #

is_weakly_amalgamable :: ExtModal2CASL -> Bool Source #

constituents :: ExtModal2CASL -> [String] Source #

isInclusionComorphism :: ExtModal2CASL -> Bool Source #

rps :: ExtModal2CASL -> Bool Source #

eps :: ExtModal2CASL -> Bool Source #

isGTC :: ExtModal2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.DFOL2CASL

Methods

sourceLogic :: DFOL2CASL -> DFOL Source #

sourceSublogic :: DFOL2CASL -> () Source #

sourceSublogicLossy :: DFOL2CASL -> () Source #

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

targetLogic :: DFOL2CASL -> CASL Source #

mapSublogic :: DFOL2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: DFOL2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: DFOL2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: DFOL2CASL -> Sign -> FORMULA -> Result CASLFORMULA Source #

map_symbol :: DFOL2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: DFOL2CASL -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source #

is_model_transportable :: DFOL2CASL -> Bool Source #

has_model_expansion :: DFOL2CASL -> Bool Source #

is_weakly_amalgamable :: DFOL2CASL -> Bool Source #

constituents :: DFOL2CASL -> [String] Source #

isInclusionComorphism :: DFOL2CASL -> Bool Source #

rps :: DFOL2CASL -> Bool Source #

eps :: DFOL2CASL -> Bool Source #

isGTC :: DFOL2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.CommonLogic2CASL

Methods

sourceLogic :: CL2CFOL -> CommonLogic Source #

sourceSublogic :: CL2CFOL -> CommonLogicSL Source #

sourceSublogicLossy :: CL2CFOL -> CommonLogicSL Source #

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

targetLogic :: CL2CFOL -> CASL Source #

mapSublogic :: CL2CFOL -> CommonLogicSL -> Maybe CASL_Sublogics Source #

map_theory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CL2CFOL -> Morphism -> Result CASLMor Source #

map_sentence :: CL2CFOL -> Sign -> TEXT_META -> Result CASLFORMULA Source #

map_symbol :: CL2CFOL -> Sign -> Symbol -> Set Symbol0 Source #

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

is_model_transportable :: CL2CFOL -> Bool Source #

has_model_expansion :: CL2CFOL -> Bool Source #

is_weakly_amalgamable :: CL2CFOL -> Bool Source #

constituents :: CL2CFOL -> [String] Source #

isInclusionComorphism :: CL2CFOL -> Bool Source #

rps :: CL2CFOL -> Bool Source #

eps :: CL2CFOL -> Bool Source #

isGTC :: CL2CFOL -> Bool Source #

Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CSMOF2CASL

Methods

sourceLogic :: CSMOF2CASL -> CSMOF Source #

sourceSublogic :: CSMOF2CASL -> () Source #

sourceSublogicLossy :: CSMOF2CASL -> () Source #

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

targetLogic :: CSMOF2CASL -> CASL Source #

mapSublogic :: CSMOF2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CSMOF2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CSMOF2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: CSMOF2CASL -> Sign -> Sen -> Result CASLFORMULA Source #

map_symbol :: CSMOF2CASL -> Sign -> () -> Set Symbol Source #

extractModel :: CSMOF2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source #

is_model_transportable :: CSMOF2CASL -> Bool Source #

has_model_expansion :: CSMOF2CASL -> Bool Source #

is_weakly_amalgamable :: CSMOF2CASL -> Bool Source #

constituents :: CSMOF2CASL -> [String] Source #

isInclusionComorphism :: CSMOF2CASL -> Bool Source #

rps :: CSMOF2CASL -> Bool Source #

eps :: CSMOF2CASL -> Bool Source #

isGTC :: CSMOF2CASL -> Bool Source #

Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.QVTR2CASL

Methods

sourceLogic :: QVTR2CASL -> QVTR Source #

sourceSublogic :: QVTR2CASL -> () Source #

sourceSublogicLossy :: QVTR2CASL -> () Source #

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

targetLogic :: QVTR2CASL -> CASL Source #

mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA Source #

map_symbol :: QVTR2CASL -> Sign -> () -> Set Symbol Source #

extractModel :: QVTR2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source #

is_model_transportable :: QVTR2CASL -> Bool Source #

has_model_expansion :: QVTR2CASL -> Bool Source #

is_weakly_amalgamable :: QVTR2CASL -> Bool Source #

constituents :: QVTR2CASL -> [String] Source #

isInclusionComorphism :: QVTR2CASL -> Bool Source #

rps :: QVTR2CASL -> Bool Source #

eps :: QVTR2CASL -> Bool Source #

isGTC :: QVTR2CASL -> Bool Source #

Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CFOL2IsabelleHOL

Methods

sourceLogic :: CFOL2IsabelleHOL -> CASL Source #

sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source #

sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source #

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

targetLogic :: CFOL2IsabelleHOL -> Isabelle Source #

mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source #

map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source #

map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source #

extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CFOL2IsabelleHOL -> Bool Source #

has_model_expansion :: CFOL2IsabelleHOL -> Bool Source #

is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source #

constituents :: CFOL2IsabelleHOL -> [String] Source #

isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source #

rps :: CFOL2IsabelleHOL -> Bool Source #

eps :: CFOL2IsabelleHOL -> Bool Source #

isGTC :: CFOL2IsabelleHOL -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2TopSort

Methods

sourceLogic :: CASL2TopSort -> CASL Source #

sourceSublogic :: CASL2TopSort -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2TopSort -> CASL_Sublogics Source #

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

targetLogic :: CASL2TopSort -> CASL Source #

mapSublogic :: CASL2TopSort -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2TopSort -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2TopSort -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2TopSort -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2TopSort -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2TopSort -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2TopSort -> Bool Source #

has_model_expansion :: CASL2TopSort -> Bool Source #

is_weakly_amalgamable :: CASL2TopSort -> Bool Source #

constituents :: CASL2TopSort -> [String] Source #

isInclusionComorphism :: CASL2TopSort -> Bool Source #

rps :: CASL2TopSort -> Bool Source #

eps :: CASL2TopSort -> Bool Source #

isGTC :: CASL2TopSort -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2SubCFOL

Methods

sourceLogic :: CASL2SubCFOL -> CASL Source #

sourceSublogic :: CASL2SubCFOL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2SubCFOL -> CASL_Sublogics Source #

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

targetLogic :: CASL2SubCFOL -> CASL Source #

mapSublogic :: CASL2SubCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2SubCFOL -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2SubCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2SubCFOL -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2SubCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2SubCFOL -> Bool Source #

has_model_expansion :: CASL2SubCFOL -> Bool Source #

is_weakly_amalgamable :: CASL2SubCFOL -> Bool Source #

constituents :: CASL2SubCFOL -> [String] Source #

isInclusionComorphism :: CASL2SubCFOL -> Bool Source #

rps :: CASL2SubCFOL -> Bool Source #

eps :: CASL2SubCFOL -> Bool Source #

isGTC :: CASL2SubCFOL -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2Skolem

Methods

sourceLogic :: CASL2Skolem -> CASL Source #

sourceSublogic :: CASL2Skolem -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Skolem -> CASL_Sublogics Source #

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

targetLogic :: CASL2Skolem -> CASL Source #

mapSublogic :: CASL2Skolem -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2Skolem -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2Skolem -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2Skolem -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2Skolem -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Skolem -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Skolem -> Bool Source #

has_model_expansion :: CASL2Skolem -> Bool Source #

is_weakly_amalgamable :: CASL2Skolem -> Bool Source #

constituents :: CASL2Skolem -> [String] Source #

isInclusionComorphism :: CASL2Skolem -> Bool Source #

rps :: CASL2Skolem -> Bool Source #

eps :: CASL2Skolem -> Bool Source #

isGTC :: CASL2Skolem -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2Prop

Methods

sourceLogic :: CASL2Prop -> CASL Source #

sourceSublogic :: CASL2Prop -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Prop -> CASL_Sublogics Source #

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

targetLogic :: CASL2Prop -> Propositional Source #

mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source #

map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #

mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #

map_morphism :: CASL2Prop -> CASLMor -> Result Morphism Source #

map_sentence :: CASL2Prop -> CASLSign -> CASLFORMULA -> Result FORMULA Source #

map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #

extractModel :: CASL2Prop -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Prop -> Bool Source #

has_model_expansion :: CASL2Prop -> Bool Source #

is_weakly_amalgamable :: CASL2Prop -> Bool Source #

constituents :: CASL2Prop -> [String] Source #

isInclusionComorphism :: CASL2Prop -> Bool Source #

rps :: CASL2Prop -> Bool Source #

eps :: CASL2Prop -> Bool Source #

isGTC :: CASL2Prop -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2Prenex

Methods

sourceLogic :: CASL2Prenex -> CASL Source #

sourceSublogic :: CASL2Prenex -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Prenex -> CASL_Sublogics Source #

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

targetLogic :: CASL2Prenex -> CASL Source #

mapSublogic :: CASL2Prenex -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2Prenex -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2Prenex -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2Prenex -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2Prenex -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Prenex -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Prenex -> Bool Source #

has_model_expansion :: CASL2Prenex -> Bool Source #

is_weakly_amalgamable :: CASL2Prenex -> Bool Source #

constituents :: CASL2Prenex -> [String] Source #

isInclusionComorphism :: CASL2Prenex -> Bool Source #

rps :: CASL2Prenex -> Bool Source #

eps :: CASL2Prenex -> Bool Source #

isGTC :: CASL2Prenex -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2PCFOL

Methods

sourceLogic :: CASL2PCFOL -> CASL Source #

sourceSublogic :: CASL2PCFOL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2PCFOL -> CASL_Sublogics Source #

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

targetLogic :: CASL2PCFOL -> CASL Source #

mapSublogic :: CASL2PCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2PCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2PCFOL -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2PCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2PCFOL -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2PCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2PCFOL -> Bool Source #

has_model_expansion :: CASL2PCFOL -> Bool Source #

is_weakly_amalgamable :: CASL2PCFOL -> Bool Source #

constituents :: CASL2PCFOL -> [String] Source #

isInclusionComorphism :: CASL2PCFOL -> Bool Source #

rps :: CASL2PCFOL -> Bool Source #

eps :: CASL2PCFOL -> Bool Source #

isGTC :: CASL2PCFOL -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2NNF

Methods

sourceLogic :: CASL2NNF -> CASL Source #

sourceSublogic :: CASL2NNF -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2NNF -> CASL_Sublogics Source #

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

targetLogic :: CASL2NNF -> CASL Source #

mapSublogic :: CASL2NNF -> CASL_Sublogics -> Maybe CASL_Sublogics Source #

map_theory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL2NNF -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL2NNF -> CASLMor -> Result CASLMor Source #

map_sentence :: CASL2NNF -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL2NNF -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2NNF -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2NNF -> Bool Source #

has_model_expansion :: CASL2NNF -> Bool Source #

is_weakly_amalgamable :: CASL2NNF -> Bool Source #

constituents :: CASL2NNF -> [String] Source #

isInclusionComorphism :: CASL2NNF -> Bool Source #

rps :: CASL2NNF -> Bool Source #

eps :: CASL2NNF -> Bool Source #

isGTC :: CASL2NNF -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2Modal

Methods

sourceLogic :: CASL2Modal -> CASL Source #

sourceSublogic :: CASL2Modal -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Modal -> CASL_Sublogics Source #

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

targetLogic :: CASL2Modal -> Modal Source #

mapSublogic :: CASL2Modal -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

mapMarkedTheory :: CASL2Modal -> (CASLSign, [Named CASLFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

map_morphism :: CASL2Modal -> CASLMor -> Result ModalMor Source #

map_sentence :: CASL2Modal -> CASLSign -> CASLFORMULA -> Result ModalFORMULA Source #

map_symbol :: CASL2Modal -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Modal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Modal -> Bool Source #

has_model_expansion :: CASL2Modal -> Bool Source #

is_weakly_amalgamable :: CASL2Modal -> Bool Source #

constituents :: CASL2Modal -> [String] Source #

isInclusionComorphism :: CASL2Modal -> Bool Source #

rps :: CASL2Modal -> Bool Source #

eps :: CASL2Modal -> Bool Source #

isGTC :: CASL2Modal -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2Hybrid

Methods

sourceLogic :: CASL2Hybrid -> CASL Source #

sourceSublogic :: CASL2Hybrid -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2Hybrid -> CASL_Sublogics Source #

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

targetLogic :: CASL2Hybrid -> Hybrid Source #

mapSublogic :: CASL2Hybrid -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

mapMarkedTheory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

map_morphism :: CASL2Hybrid -> CASLMor -> Result HybridMor Source #

map_sentence :: CASL2Hybrid -> CASLSign -> CASLFORMULA -> Result HybridFORMULA Source #

map_symbol :: CASL2Hybrid -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2Hybrid -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2Hybrid -> Bool Source #

has_model_expansion :: CASL2Hybrid -> Bool Source #

is_weakly_amalgamable :: CASL2Hybrid -> Bool Source #

constituents :: CASL2Hybrid -> [String] Source #

isInclusionComorphism :: CASL2Hybrid -> Bool Source #

rps :: CASL2Hybrid -> Bool Source #

eps :: CASL2Hybrid -> Bool Source #

isGTC :: CASL2Hybrid -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2HasCASL

Methods

sourceLogic :: CASL2HasCASL -> CASL Source #

sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source #

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

targetLogic :: CASL2HasCASL -> HasCASL Source #

mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source #

map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source #

mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source #

map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source #

map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source #

extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2HasCASL -> Bool Source #

has_model_expansion :: CASL2HasCASL -> Bool Source #

is_weakly_amalgamable :: CASL2HasCASL -> Bool Source #

constituents :: CASL2HasCASL -> [String] Source #

isInclusionComorphism :: CASL2HasCASL -> Bool Source #

rps :: CASL2HasCASL -> Bool Source #

eps :: CASL2HasCASL -> Bool Source #

isGTC :: CASL2HasCASL -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2ExtModal

Methods

sourceLogic :: CASL2ExtModal -> CASL Source #

sourceSublogic :: CASL2ExtModal -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2ExtModal -> CASL_Sublogics Source #

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

targetLogic :: CASL2ExtModal -> ExtModal Source #

mapSublogic :: CASL2ExtModal -> CASL_Sublogics -> Maybe ExtModalSL Source #

map_theory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

mapMarkedTheory :: CASL2ExtModal -> (CASLSign, [Named CASLFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

map_morphism :: CASL2ExtModal -> CASLMor -> Result ExtModalMorph Source #

map_sentence :: CASL2ExtModal -> CASLSign -> CASLFORMULA -> Result ExtModalFORMULA Source #

map_symbol :: CASL2ExtModal -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2ExtModal -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2ExtModal -> Bool Source #

has_model_expansion :: CASL2ExtModal -> Bool Source #

is_weakly_amalgamable :: CASL2ExtModal -> Bool Source #

constituents :: CASL2ExtModal -> [String] Source #

isInclusionComorphism :: CASL2ExtModal -> Bool Source #

rps :: CASL2ExtModal -> Bool Source #

eps :: CASL2ExtModal -> Bool Source #

isGTC :: CASL2ExtModal -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2CspCASL

Methods

sourceLogic :: CASL2CspCASL -> CASL Source #

sourceSublogic :: CASL2CspCASL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2CspCASL -> CASL_Sublogics Source #

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

targetLogic :: CASL2CspCASL -> CspCASL Source #

mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

mapMarkedTheory :: CASL2CspCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism Source #

map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen Source #

map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol Source #

extractModel :: CASL2CspCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2CspCASL -> Bool Source #

has_model_expansion :: CASL2CspCASL -> Bool Source #

is_weakly_amalgamable :: CASL2CspCASL -> Bool Source #

constituents :: CASL2CspCASL -> [String] Source #

isInclusionComorphism :: CASL2CspCASL -> Bool Source #

rps :: CASL2CspCASL -> Bool Source #

eps :: CASL2CspCASL -> Bool Source #

isGTC :: CASL2CspCASL -> Bool 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 # 
Instance details

Defined in Comorphisms.Adl2CASL

Methods

sourceLogic :: Adl2CASL -> Adl Source #

sourceSublogic :: Adl2CASL -> () Source #

sourceSublogicLossy :: Adl2CASL -> () Source #

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

targetLogic :: Adl2CASL -> CASL Source #

mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics Source #

map_theory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: Adl2CASL -> Morphism -> Result CASLMor Source #

map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA Source #

map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol0 Source #

extractModel :: Adl2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source #

is_model_transportable :: Adl2CASL -> Bool Source #

has_model_expansion :: Adl2CASL -> Bool Source #

is_weakly_amalgamable :: Adl2CASL -> Bool Source #

constituents :: Adl2CASL -> [String] Source #

isInclusionComorphism :: Adl2CASL -> Bool Source #

rps :: Adl2CASL -> Bool Source #

eps :: Adl2CASL -> Bool Source #

isGTC :: Adl2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2CoCASL

Methods

sourceLogic :: CASL2CoCASL -> CASL Source #

sourceSublogic :: CASL2CoCASL -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2CoCASL -> CASL_Sublogics Source #

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

targetLogic :: CASL2CoCASL -> CoCASL Source #

mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics Source #

map_theory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

mapMarkedTheory :: CASL2CoCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor Source #

map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA Source #

map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2CoCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2CoCASL -> Bool Source #

has_model_expansion :: CASL2CoCASL -> Bool Source #

is_weakly_amalgamable :: CASL2CoCASL -> Bool Source #

constituents :: CASL2CoCASL -> [String] Source #

isInclusionComorphism :: CASL2CoCASL -> Bool Source #

rps :: CASL2CoCASL -> Bool Source #

eps :: CASL2CoCASL -> Bool Source #

isGTC :: CASL2CoCASL -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL_DL2CASL

Methods

sourceLogic :: CASL_DL2CASL -> CASL_DL Source #

sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL Source #

sourceSublogicLossy :: CASL_DL2CASL -> CASL_DL_SL Source #

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

targetLogic :: CASL_DL2CASL -> CASL Source #

mapSublogic :: CASL_DL2CASL -> CASL_DL_SL -> Maybe CASL_Sublogics Source #

map_theory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

mapMarkedTheory :: CASL_DL2CASL -> (DLSign, [Named DLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

map_morphism :: CASL_DL2CASL -> DLMor -> Result CASLMor Source #

map_sentence :: CASL_DL2CASL -> DLSign -> DLFORMULA -> Result CASLFORMULA Source #

map_symbol :: CASL_DL2CASL -> DLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL_DL2CASL -> DLSign -> ProofTree -> Result (DLSign, [Named DLFORMULA]) Source #

is_model_transportable :: CASL_DL2CASL -> Bool Source #

has_model_expansion :: CASL_DL2CASL -> Bool Source #

is_weakly_amalgamable :: CASL_DL2CASL -> Bool Source #

constituents :: CASL_DL2CASL -> [String] Source #

isInclusionComorphism :: CASL_DL2CASL -> Bool Source #

rps :: CASL_DL2CASL -> Bool Source #

eps :: CASL_DL2CASL -> Bool Source #

isGTC :: CASL_DL2CASL -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2VSERefine

Methods

sourceLogic :: CASL2VSERefine -> CASL Source #

sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source #

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

targetLogic :: CASL2VSERefine -> VSE Source #

mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source #

map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2VSERefine -> Bool Source #

has_model_expansion :: CASL2VSERefine -> Bool Source #

is_weakly_amalgamable :: CASL2VSERefine -> Bool Source #

constituents :: CASL2VSERefine -> [String] Source #

isInclusionComorphism :: CASL2VSERefine -> Bool Source #

rps :: CASL2VSERefine -> Bool Source #

eps :: CASL2VSERefine -> Bool Source #

isGTC :: CASL2VSERefine -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2VSEImport

Methods

sourceLogic :: CASL2VSEImport -> CASL Source #

sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source #

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

targetLogic :: CASL2VSEImport -> VSE Source #

mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source #

map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2VSEImport -> Bool Source #

has_model_expansion :: CASL2VSEImport -> Bool Source #

is_weakly_amalgamable :: CASL2VSEImport -> Bool Source #

constituents :: CASL2VSEImport -> [String] Source #

isInclusionComorphism :: CASL2VSEImport -> Bool Source #

rps :: CASL2VSEImport -> Bool Source #

eps :: CASL2VSEImport -> Bool Source #

isGTC :: CASL2VSEImport -> Bool 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 # 
Instance details

Defined in Comorphisms.CASL2VSE

Methods

sourceLogic :: CASL2VSE -> CASL Source #

sourceSublogic :: CASL2VSE -> CASL_Sublogics Source #

sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source #

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

targetLogic :: CASL2VSE -> VSE Source #

mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source #

map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source #

map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source #

map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source #

map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source #

extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source #

is_model_transportable :: CASL2VSE -> Bool Source #

has_model_expansion :: CASL2VSE -> Bool Source #

is_weakly_amalgamable :: CASL2VSE -> Bool Source #

constituents :: CASL2VSE -> [String] Source #

isInclusionComorphism :: CASL2VSE -> Bool Source #

rps :: CASL2VSE -> Bool Source #

eps :: CASL2VSE -> Bool Source #

isGTC :: CASL2VSE -> Bool Source #

Comorphism DMU2OWL2 DMU () Text () () () Text (DefaultMorphism Text) () () () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in OWL2.DMU2OWL2

Methods

sourceLogic :: DMU2OWL2 -> DMU Source #

sourceSublogic :: DMU2OWL2 -> () Source #

sourceSublogicLossy :: DMU2OWL2 -> () Source #

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

targetLogic :: DMU2OWL2 -> OWL2 Source #

mapSublogic :: DMU2OWL2 -> () -> Maybe ProfSub Source #

map_theory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source #

mapMarkedTheory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom]) Source #

map_morphism :: DMU2OWL2 -> DefaultMorphism Text -> Result OWLMorphism Source #

map_sentence :: DMU2OWL2 -> Text -> () -> Result Axiom Source #

map_symbol :: DMU2OWL2 -> Text -> () -> Set Entity Source #

extractModel :: DMU2OWL2 -> Text -> ProofTree -> Result (Text, [Named ()]) Source #

is_model_transportable :: DMU2OWL2 -> Bool Source #

has_model_expansion :: DMU2OWL2 -> Bool Source #

is_weakly_amalgamable :: DMU2OWL2 -> Bool Source #

constituents :: DMU2OWL2 -> [String] Source #

isInclusionComorphism :: DMU2OWL2 -> Bool Source #

rps :: DMU2OWL2 -> Bool Source #

eps :: DMU2OWL2 -> Bool Source #

isGTC :: DMU2OWL2 -> Bool 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 # 
Instance details

Defined in Comorphisms.SoftFOL2CommonLogic

Methods

sourceLogic :: SoftFOL2CommonLogic -> SoftFOL Source #

sourceSublogic :: SoftFOL2CommonLogic -> () Source #

sourceSublogicLossy :: SoftFOL2CommonLogic -> () Source #

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

targetLogic :: SoftFOL2CommonLogic -> CommonLogic Source #

mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL Source #

map_theory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source #

mapMarkedTheory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source #

map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism Source #

map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META Source #

map_symbol :: SoftFOL2CommonLogic -> Sign -> SFSymbol -> Set Symbol Source #

extractModel :: SoftFOL2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source #

is_model_transportable :: SoftFOL2CommonLogic -> Bool Source #

has_model_expansion :: SoftFOL2CommonLogic -> Bool Source #

is_weakly_amalgamable :: SoftFOL2CommonLogic -> Bool Source #

constituents :: SoftFOL2CommonLogic -> [String] Source #

isInclusionComorphism :: SoftFOL2CommonLogic -> Bool Source #

rps :: SoftFOL2CommonLogic -> Bool Source #

eps :: SoftFOL2CommonLogic -> Bool Source #

isGTC :: SoftFOL2CommonLogic -> Bool Source #

Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 
Instance details

Defined in SoftFOL.Logic_SoftFOL

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 #

sublogicOfTheo :: SoftFOL -> (Sign, [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 # 
Instance details

Defined in Modifications.ModalEmbedding

Methods

tauSigma :: MODAL_EMBEDDING -> CASLSign -> Result CASLMor Source #

sourceComorphism :: MODAL_EMBEDDING -> InclComorphism CASL CASL_Sublogics Source #

targetComorphism :: MODAL_EMBEDDING -> CompComorphism CASL2Modal Modal2CASL Source #

type Rep ProofTree 
Instance details

Defined in ATC.ProofTree

type Rep ProofTree = D1 ('MetaData "ProofTree" "Common.ProofTree" "main" 'False) (C1 ('MetaCons "ProofTree" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "ProofGraph" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Gr ProofGraphNode Int))))

type ProofGraphNode = Either String (String, String) Source #

emptyProofTree :: ProofTree Source #

Orphan instances

ShATermConvertible (Gr ProofGraphNode Int) Source # 
Instance details

Methods

toShATermAux :: ATermTable -> Gr ProofGraphNode Int -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Gr ProofGraphNode Int] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Gr ProofGraphNode Int)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Gr ProofGraphNode Int])