Copyright	(c) Jonathan von Schroeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	<jonathan.von_schroeder@dfki.de>
Stability	experimental
Portability	portable
Safe Haskell	Safe

QBF.AS_BASIC_QBF

Description

Definition of abstract syntax for propositional logic extended with QBFs

Ref. http://en.wikipedia.org/wiki/Propositional_logic http://www.voronkov.com/lics.cgi

Synopsis

Documentation

data FORMULA Source #

Datatype for QBF formulas

Instances

Eq FORMULA Source #
Methods (==) :: FORMULA -> FORMULA -> Bool (/=) :: FORMULA -> FORMULA -> Bool
Data FORMULA Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FORMULA -> c FORMULA gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FORMULA toConstr :: FORMULA -> Constr dataTypeOf :: FORMULA -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FORMULA) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA) gmapT :: (forall b. Data b => b -> b) -> FORMULA -> FORMULA gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FORMULA -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FORMULA -> r gmapQ :: (forall d. Data d => d -> u) -> FORMULA -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FORMULA -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
Ord FORMULA Source #
Methods compare :: FORMULA -> FORMULA -> Ordering (<) :: FORMULA -> FORMULA -> Bool (<=) :: FORMULA -> FORMULA -> Bool (>) :: FORMULA -> FORMULA -> Bool (>=) :: FORMULA -> FORMULA -> Bool max :: FORMULA -> FORMULA -> FORMULA min :: FORMULA -> FORMULA -> FORMULA
Show FORMULA Source #
Methods showsPrec :: Int -> FORMULA -> ShowS show :: FORMULA -> String showList :: [FORMULA] -> ShowS
GetRange FORMULA Source #
Methods getRange :: FORMULA -> Range Source # rangeSpan :: FORMULA -> [Pos] Source #
Pretty FORMULA Source #
Methods pretty :: FORMULA -> Doc Source # pretties :: [FORMULA] -> Doc Source #
Sentences QBF FORMULA Sign Morphism Symbol Source #	Instance of Sentences for propositional logic
Methods map_sen :: QBF -> Morphism -> FORMULA -> Result FORMULA Source # simplify_sen :: QBF -> Sign -> FORMULA -> FORMULA Source # negation :: QBF -> FORMULA -> Maybe FORMULA Source # print_sign :: QBF -> Sign -> Doc Source # print_named :: QBF -> Named FORMULA -> Doc Source # sym_of :: QBF -> Sign -> [Set Symbol] Source # mostSymsOf :: QBF -> Sign -> [Symbol] Source # symmap_of :: QBF -> Morphism -> EndoMap Symbol Source # sym_name :: QBF -> Symbol -> Id Source # sym_label :: QBF -> Symbol -> Maybe String Source # fullSymName :: QBF -> Symbol -> String Source # symKind :: QBF -> Symbol -> String Source # symsOfSen :: QBF -> Sign -> FORMULA -> [Symbol] Source # pair_symbols :: QBF -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #
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 #
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 FORMULA]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: Prop2QBF -> Morphism -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) 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 #
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 #
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 FORMULA]) Source # mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: QBF2Prop -> Morphism -> Result Morphism Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol 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 #

data BASICITEMS Source #

Constructors

PredDecl PREDITEM
AxiomItems [Annoted FORMULA]

Instances

Data BASICITEMS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASICITEMS toConstr :: BASICITEMS -> Constr dataTypeOf :: BASICITEMS -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BASICITEMS) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICITEMS) gmapT :: (forall b. Data b => b -> b) -> BASICITEMS -> BASICITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> BASICITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASICITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
Show BASICITEMS Source #
Methods showsPrec :: Int -> BASICITEMS -> ShowS show :: BASICITEMS -> String showList :: [BASICITEMS] -> ShowS
GetRange BASICITEMS Source #
Methods getRange :: BASICITEMS -> Range Source # rangeSpan :: BASICITEMS -> [Pos] Source #
Pretty BASICITEMS Source #
Methods pretty :: BASICITEMS -> Doc Source # pretties :: [BASICITEMS] -> Doc Source #

newtype BASICSPEC Source #

Constructors

BasicSpec [Annoted BASICITEMS]

Instances

Data BASICSPEC Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASICSPEC -> c BASICSPEC gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASICSPEC toConstr :: BASICSPEC -> Constr dataTypeOf :: BASICSPEC -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BASICSPEC) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICSPEC) gmapT :: (forall b. Data b => b -> b) -> BASICSPEC -> BASICSPEC gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r gmapQ :: (forall d. Data d => d -> u) -> BASICSPEC -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASICSPEC -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
Show BASICSPEC Source #
Methods showsPrec :: Int -> BASICSPEC -> ShowS show :: BASICSPEC -> String showList :: [BASICSPEC] -> ShowS
GetRange BASICSPEC Source #
Methods getRange :: BASICSPEC -> Range Source # rangeSpan :: BASICSPEC -> [Pos] Source #
Pretty BASICSPEC Source #
Methods pretty :: BASICSPEC -> Doc Source # pretties :: [BASICSPEC] -> Doc Source #
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #	Syntax of Propositional logic
Methods parsersAndPrinters :: QBF -> Map String (PrefixMap -> AParser st BASICSPEC, BASICSPEC -> Doc) Source # parse_basic_spec :: QBF -> Maybe (PrefixMap -> AParser st BASICSPEC) Source # parseSingleSymbItem :: QBF -> Maybe (AParser st SYMBITEMS) Source # parse_symb_items :: QBF -> Maybe (AParser st SYMBITEMS) Source # parse_symb_map_items :: QBF -> Maybe (AParser st SYMBMAPITEMS) Source # toItem :: QBF -> BASICSPEC -> Item Source # symb_items_name :: QBF -> SYMBITEMS -> [String] Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #
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 #
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 FORMULA]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: Prop2QBF -> Morphism -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) 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 #
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 #
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 FORMULA]) Source # mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: QBF2Prop -> Morphism -> Result Morphism Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol 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 #

data SYMBITEMS Source #

Constructors

SymbItems [SYMB] Range

Instances

Eq SYMBITEMS Source #
Methods (==) :: SYMBITEMS -> SYMBITEMS -> Bool (/=) :: SYMBITEMS -> SYMBITEMS -> Bool
Data SYMBITEMS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMBITEMS -> c SYMBITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBITEMS toConstr :: SYMBITEMS -> Constr dataTypeOf :: SYMBITEMS -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SYMBITEMS) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBITEMS) gmapT :: (forall b. Data b => b -> b) -> SYMBITEMS -> SYMBITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMBITEMS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMBITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> SYMBITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMBITEMS -> m SYMBITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBITEMS -> m SYMBITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBITEMS -> m SYMBITEMS
Ord SYMBITEMS Source #
Methods compare :: SYMBITEMS -> SYMBITEMS -> Ordering (<) :: SYMBITEMS -> SYMBITEMS -> Bool (<=) :: SYMBITEMS -> SYMBITEMS -> Bool (>) :: SYMBITEMS -> SYMBITEMS -> Bool (>=) :: SYMBITEMS -> SYMBITEMS -> Bool max :: SYMBITEMS -> SYMBITEMS -> SYMBITEMS min :: SYMBITEMS -> SYMBITEMS -> SYMBITEMS
Show SYMBITEMS Source #
Methods showsPrec :: Int -> SYMBITEMS -> ShowS show :: SYMBITEMS -> String showList :: [SYMBITEMS] -> ShowS
GetRange SYMBITEMS Source #
Methods getRange :: SYMBITEMS -> Range Source # rangeSpan :: SYMBITEMS -> [Pos] Source #
Pretty SYMBITEMS Source #
Methods pretty :: SYMBITEMS -> Doc Source # pretties :: [SYMBITEMS] -> Doc Source #
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #	Syntax of Propositional logic
Methods parsersAndPrinters :: QBF -> Map String (PrefixMap -> AParser st BASICSPEC, BASICSPEC -> Doc) Source # parse_basic_spec :: QBF -> Maybe (PrefixMap -> AParser st BASICSPEC) Source # parseSingleSymbItem :: QBF -> Maybe (AParser st SYMBITEMS) Source # parse_symb_items :: QBF -> Maybe (AParser st SYMBITEMS) Source # parse_symb_map_items :: QBF -> Maybe (AParser st SYMBMAPITEMS) Source # toItem :: QBF -> BASICSPEC -> Item Source # symb_items_name :: QBF -> SYMBITEMS -> [String] Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #
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 #
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 FORMULA]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: Prop2QBF -> Morphism -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) 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 #
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 #
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 FORMULA]) Source # mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: QBF2Prop -> Morphism -> Result Morphism Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol 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 #

newtype SYMB Source #

Constructors

SymbId Token

Instances

Eq SYMB Source #
Methods (==) :: SYMB -> SYMB -> Bool (/=) :: SYMB -> SYMB -> Bool
Data SYMB Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB -> c SYMB gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB toConstr :: SYMB -> Constr dataTypeOf :: SYMB -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB) gmapT :: (forall b. Data b => b -> b) -> SYMB -> SYMB gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB
Ord SYMB Source #
Methods compare :: SYMB -> SYMB -> Ordering (<) :: SYMB -> SYMB -> Bool (<=) :: SYMB -> SYMB -> Bool (>) :: SYMB -> SYMB -> Bool (>=) :: SYMB -> SYMB -> Bool max :: SYMB -> SYMB -> SYMB min :: SYMB -> SYMB -> SYMB
Show SYMB Source #
Methods showsPrec :: Int -> SYMB -> ShowS show :: SYMB -> String showList :: [SYMB] -> ShowS
GetRange SYMB Source #
Methods getRange :: SYMB -> Range Source # rangeSpan :: SYMB -> [Pos] Source #
Pretty SYMB Source #
Methods pretty :: SYMB -> Doc Source # pretties :: [SYMB] -> Doc Source #

data SYMBMAPITEMS Source #

Constructors

SymbMapItems [SYMBORMAP] Range

Instances

Eq SYMBMAPITEMS Source #
Methods (==) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (/=) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool
Data SYMBMAPITEMS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMBMAPITEMS -> c SYMBMAPITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBMAPITEMS toConstr :: SYMBMAPITEMS -> Constr dataTypeOf :: SYMBMAPITEMS -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SYMBMAPITEMS) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBMAPITEMS) gmapT :: (forall b. Data b => b -> b) -> SYMBMAPITEMS -> SYMBMAPITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMBMAPITEMS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMBMAPITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> SYMBMAPITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBMAPITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMBMAPITEMS -> m SYMBMAPITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBMAPITEMS -> m SYMBMAPITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBMAPITEMS -> m SYMBMAPITEMS
Ord SYMBMAPITEMS Source #
Methods compare :: SYMBMAPITEMS -> SYMBMAPITEMS -> Ordering (<) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (<=) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (>) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (>=) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool max :: SYMBMAPITEMS -> SYMBMAPITEMS -> SYMBMAPITEMS min :: SYMBMAPITEMS -> SYMBMAPITEMS -> SYMBMAPITEMS
Show SYMBMAPITEMS Source #
Methods showsPrec :: Int -> SYMBMAPITEMS -> ShowS show :: SYMBMAPITEMS -> String showList :: [SYMBMAPITEMS] -> ShowS
GetRange SYMBMAPITEMS Source #
Methods getRange :: SYMBMAPITEMS -> Range Source # rangeSpan :: SYMBMAPITEMS -> [Pos] Source #
Pretty SYMBMAPITEMS Source #
Methods pretty :: SYMBMAPITEMS -> Doc Source # pretties :: [SYMBMAPITEMS] -> Doc Source #
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #	Syntax of Propositional logic
Methods parsersAndPrinters :: QBF -> Map String (PrefixMap -> AParser st BASICSPEC, BASICSPEC -> Doc) Source # parse_basic_spec :: QBF -> Maybe (PrefixMap -> AParser st BASICSPEC) Source # parseSingleSymbItem :: QBF -> Maybe (AParser st SYMBITEMS) Source # parse_symb_items :: QBF -> Maybe (AParser st SYMBITEMS) Source # parse_symb_map_items :: QBF -> Maybe (AParser st SYMBMAPITEMS) Source # toItem :: QBF -> BASICSPEC -> Item Source # symb_items_name :: QBF -> SYMBITEMS -> [String] Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #
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 #
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 FORMULA]) -> Result (Sign, [Named FORMULA]) Source # mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: Prop2QBF -> Morphism -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) 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 #
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 #
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 FORMULA]) Source # mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # map_morphism :: QBF2Prop -> Morphism -> Result Morphism Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol 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 #

data SYMBORMAP Source #

Constructors

Symb SYMB
SymbMap SYMB SYMB Range

Instances

Eq SYMBORMAP Source #
Methods (==) :: SYMBORMAP -> SYMBORMAP -> Bool (/=) :: SYMBORMAP -> SYMBORMAP -> Bool
Data SYMBORMAP Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBORMAP toConstr :: SYMBORMAP -> Constr dataTypeOf :: SYMBORMAP -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SYMBORMAP) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBORMAP) gmapT :: (forall b. Data b => b -> b) -> SYMBORMAP -> SYMBORMAP gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r gmapQ :: (forall d. Data d => d -> u) -> SYMBORMAP -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBORMAP -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
Ord SYMBORMAP Source #
Methods compare :: SYMBORMAP -> SYMBORMAP -> Ordering (<) :: SYMBORMAP -> SYMBORMAP -> Bool (<=) :: SYMBORMAP -> SYMBORMAP -> Bool (>) :: SYMBORMAP -> SYMBORMAP -> Bool (>=) :: SYMBORMAP -> SYMBORMAP -> Bool max :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP min :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP
Show SYMBORMAP Source #
Methods showsPrec :: Int -> SYMBORMAP -> ShowS show :: SYMBORMAP -> String showList :: [SYMBORMAP] -> ShowS
GetRange SYMBORMAP Source #
Methods getRange :: SYMBORMAP -> Range Source # rangeSpan :: SYMBORMAP -> [Pos] Source #
Pretty SYMBORMAP Source #
Methods pretty :: SYMBORMAP -> Doc Source # pretties :: [SYMBORMAP] -> Doc Source #

data PREDITEM Source #

predicates = propositions

Constructors

PredItem [Token] Range

Instances

Data PREDITEM Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PREDITEM -> c PREDITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PREDITEM toConstr :: PREDITEM -> Constr dataTypeOf :: PREDITEM -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c PREDITEM) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PREDITEM) gmapT :: (forall b. Data b => b -> b) -> PREDITEM -> PREDITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r gmapQ :: (forall d. Data d => d -> u) -> PREDITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PREDITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
Show PREDITEM Source #
Methods showsPrec :: Int -> PREDITEM -> ShowS show :: PREDITEM -> String showList :: [PREDITEM] -> ShowS
GetRange PREDITEM Source #
Methods getRange :: PREDITEM -> Range Source # rangeSpan :: PREDITEM -> [Pos] Source #
Pretty PREDITEM Source #
Methods pretty :: PREDITEM -> Doc Source # pretties :: [PREDITEM] -> Doc Source #

isPrimForm :: FORMULA -> Bool Source #

data ID Source #

Constructors

ID Token (Maybe Token)

Instances

Eq ID Source #
Methods (==) :: ID -> ID -> Bool (/=) :: ID -> ID -> Bool
Data ID Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ID -> c ID gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ID toConstr :: ID -> Constr dataTypeOf :: ID -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c ID) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ID) gmapT :: (forall b. Data b => b -> b) -> ID -> ID gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r gmapQ :: (forall d. Data d => d -> u) -> ID -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ID -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ID -> m ID gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ID -> m ID gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ID -> m ID
GetRange ID Source #
Methods getRange :: ID -> Range Source # rangeSpan :: ID -> [Pos] Source #

FalseAtom Range
TrueAtom Range
Predication Token
Negation FORMULA Range
Conjunction [FORMULA] Range
Disjunction [FORMULA] Range
Implication FORMULA FORMULA Range
Equivalence FORMULA FORMULA Range
ForAll [Token] FORMULA Range
Exists [Token] FORMULA Range