Hets - the Heterogeneous Tool Set
Copyright (c) Dominik Luecke Uni Bremen 2007 GPLv2 or higher, see LICENSE.txt luecke@informatik.uni-bremen.de experimental non-portable (imports Logic.Logic) Safe

Propositional.Sublogic

Description

Sublogics for Propositional Logic

Synopsis

# Documentation

determines sublogic for basic spec

types of propositional formulae

Constructors

 PlainFormula HornClause

#### Instances

Instances details
 Source # Instance detailsDefined in Propositional.Sublogic Methods(==) :: PropFormulae -> PropFormulae -> Bool(/=) :: PropFormulae -> PropFormulae -> Bool Data PropFormulae Source # Instance detailsDefined in Propositional.Sublogic Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PropFormulae -> c PropFormulaegunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PropFormulaetoConstr :: PropFormulae -> ConstrdataTypeOf :: PropFormulae -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PropFormulae)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropFormulae)gmapT :: (forall b. Data b => b -> b) -> PropFormulae -> PropFormulaegmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropFormulae -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropFormulae -> rgmapQ :: (forall d. Data d => d -> u) -> PropFormulae -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> PropFormulae -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulaegmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulaegmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae Ord PropFormulae Source # Instance detailsDefined in Propositional.Sublogic Methodscompare :: PropFormulae -> PropFormulae -> Ordering(<) :: PropFormulae -> PropFormulae -> Bool(<=) :: PropFormulae -> PropFormulae -> Bool(>) :: PropFormulae -> PropFormulae -> Bool(>=) :: PropFormulae -> PropFormulae -> Bool Show PropFormulae Source # Instance detailsDefined in Propositional.Sublogic MethodsshowsPrec :: Int -> PropFormulae -> ShowSshow :: PropFormulae -> StringshowList :: [PropFormulae] -> ShowS Generic PropFormulae Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep PropFormulae :: Type -> Type Methodsfrom :: PropFormulae -> Rep PropFormulae xto :: Rep PropFormulae x -> PropFormulae FromJSON PropFormulae Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser PropFormulaeparseJSONList :: Value -> Parser [PropFormulae] ToJSON PropFormulae Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: PropFormulae -> ValuetoEncoding :: PropFormulae -> EncodingtoJSONList :: [PropFormulae] -> ValuetoEncodingList :: [PropFormulae] -> Encoding ShATermConvertible PropFormulae Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> PropFormulae -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [PropFormulae] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, PropFormulae)fromShATermList' :: Int -> ATermTable -> (ATermTable, [PropFormulae]) type Rep PropFormulae Instance detailsDefined in Propositional.ATC_Propositional type Rep PropFormulae = D1 ('MetaData "PropFormulae" "Propositional.Sublogic" "main" 'False) (C1 ('MetaCons "PlainFormula" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HornClause" 'PrefixI 'False) (U1 :: Type -> Type))

data PropSL Source #

sublogics for propositional logic

Constructors

 PropSL Fieldsformat :: PropFormulae

#### Instances

Instances details
 Eq PropSL Source # Instance detailsDefined in Propositional.Sublogic Methods(==) :: PropSL -> PropSL -> Bool(/=) :: PropSL -> PropSL -> Bool Data PropSL Source # Instance detailsDefined in Propositional.Sublogic Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PropSL -> c PropSLgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PropSLtoConstr :: PropSL -> ConstrdataTypeOf :: PropSL -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PropSL)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL)gmapT :: (forall b. Data b => b -> b) -> PropSL -> PropSLgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> rgmapQ :: (forall d. Data d => d -> u) -> PropSL -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> PropSL -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> PropSL -> m PropSLgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PropSL -> m PropSLgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PropSL -> m PropSL Ord PropSL Source # Instance detailsDefined in Propositional.Sublogic Methodscompare :: PropSL -> PropSL -> Ordering(<) :: PropSL -> PropSL -> Bool(<=) :: PropSL -> PropSL -> Bool(>) :: PropSL -> PropSL -> Bool(>=) :: PropSL -> PropSL -> Boolmax :: PropSL -> PropSL -> PropSLmin :: PropSL -> PropSL -> PropSL Show PropSL Source # Instance detailsDefined in Propositional.Sublogic MethodsshowsPrec :: Int -> PropSL -> ShowSshow :: PropSL -> StringshowList :: [PropSL] -> ShowS Generic PropSL Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep PropSL :: Type -> Type Methodsfrom :: PropSL -> Rep PropSL xto :: Rep PropSL x -> PropSL FromJSON PropSL Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser PropSLparseJSONList :: Value -> Parser [PropSL] ToJSON PropSL Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: PropSL -> ValuetoEncoding :: PropSL -> EncodingtoJSONList :: [PropSL] -> ValuetoEncodingList :: [PropSL] -> Encoding ShATermConvertible PropSL Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> PropSL -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [PropSL] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, PropSL)fromShATermList' :: Int -> ATermTable -> (ATermTable, [PropSL]) Source # Instance detailsDefined in Propositional.Logic_Propositional MethodssublogicName :: PropSL -> String Source # Source # Sublogics Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional MethodsprojectSublogicM :: PropSL -> FORMULA -> Maybe FORMULA Source # Source # Instance detailsDefined in Propositional.Logic_Propositional MethodsprojectSublogicM :: PropSL -> Symbol -> Maybe Symbol Source # Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance of Logic for propositional logc Instance detailsDefined in Propositional.Logic_Propositional Methodsparse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #data_logic :: Propositional -> Maybe AnyLogic Source #bottomSublogic :: Propositional -> Maybe PropSL Source #parseSublogic :: Propositional -> String -> Maybe PropSL Source #default_prover :: Propositional -> String Source #syntaxTable :: Propositional -> Sign -> Maybe SyntaxTable Source #omdoc_metatheory :: Propositional -> Maybe OMCD Source #export_symToOmdoc :: Propositional -> NameMap Symbol -> Symbol -> String -> 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 # Source # Instance detailsDefined in OWL2.Propositional2OWL2 MethodsminSourceTheory :: Propositional2OWL2 -> Maybe (LibName, String) Source #map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #constituents :: Propositional2OWL2 -> [String] Source #rps :: Propositional2OWL2 -> Bool Source #eps :: Propositional2OWL2 -> Bool Source #isGTC :: Propositional2OWL2 -> Bool Source # Source # Instance detailsDefined in Comorphisms.QBF2Prop MethodsminSourceTheory :: QBF2Prop -> Maybe (LibName, String) 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_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 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 # Source # Instance detailsDefined in Comorphisms.Prop2QBF MethodsminSourceTheory :: Prop2QBF -> Maybe (LibName, String) 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_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol 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 # Source # Instance detailsDefined in Comorphisms.Prop2CommonLogic MethodsminSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source #map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #constituents :: Prop2CommonLogic -> [String] Source #rps :: Prop2CommonLogic -> Bool Source #eps :: Prop2CommonLogic -> Bool Source #isGTC :: Prop2CommonLogic -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CASL MethodsminSourceTheory :: Prop2CASL -> Maybe (LibName, String) 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_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: Prop2CASL -> Bool Source #constituents :: Prop2CASL -> [String] Source #rps :: Prop2CASL -> Bool Source #eps :: Prop2CASL -> Bool Source #isGTC :: Prop2CASL -> Bool Source # Source # Instance detailsDefined in Comorphisms.CASL2Prop MethodsminSourceTheory :: CASL2Prop -> Maybe (LibName, String) 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_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #has_model_expansion :: CASL2Prop -> Bool Source #constituents :: CASL2Prop -> [String] Source #rps :: CASL2Prop -> Bool Source #eps :: CASL2Prop -> Bool Source #isGTC :: CASL2Prop -> Bool Source # type Rep PropSL Instance detailsDefined in Propositional.ATC_Propositional type Rep PropSL = D1 ('MetaData "PropSL" "Propositional.Sublogic" "main" 'False) (C1 ('MetaCons "PropSL" 'PrefixI 'True) (S1 ('MetaSel ('Just "format") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PropFormulae)))

all sublogics

determines the sublogic for a Signature

determines sublogic for formula

determines the sublogic for symbols

determines the sublogic for Symbol items

determines the sublogic for a morphism

determines the sublogic for symbol map items

isProp :: PropSL -> Bool Source #

isHC :: PropSL -> Bool Source #