Copyright	(c) Mihai Codescu 2016
License	GPLv2 or higher, see LICENSE.txt
Maintainer	codescu@iws.cs.uni-magdeburg.de
Stability	provisional
Portability	non-portable (imports Logic.Comorphism)
Safe Haskell	None

Comorphisms.CASL2Skolem

Description

removing existential quantifiers from every formula follows http://resources.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ss10/script/lecture10.pdf

Documentation

data CASL2Skolem Source #

Constructors

CASL2Skolem

Instances

Instances details

Show CASL2Skolem Source #
Instance details Defined in Comorphisms.CASL2Skolem Methods showsPrec :: Int -> CASL2Skolem -> ShowS show :: CASL2Skolem -> String showList :: [CASL2Skolem] -> ShowS
Language CASL2Skolem Source #
Instance details Defined in Comorphisms.CASL2Skolem Methods language_name :: CASL2Skolem -> String Source # description :: CASL2Skolem -> String 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 #

mapSentence :: CASLSign -> CASLFORMULA -> Result CASLFORMULA Source #

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

mkSkolemFunction :: Int -> Id Source #

replaceBoundVars :: [(VAR, SORT)] -> [(VAR, SORT)] -> Int -> CASLFORMULA -> (CASLSign, CASLFORMULA) Source #

skolemize :: Int -> [(VAR, SORT)] -> CASLSign -> CASLSign -> CASLFORMULA -> (Int, CASLSign, CASLFORMULA) Source #