Copyright	(c) Eugen Kuksa and Uni Bremen 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	eugenk@informatik.uni-bremen.de
Stability	experimental
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.Prop2CommonLogic

Description

The translating comorphism from Propositional to CommonLogic.

Synopsis

data Prop2CommonLogic = Prop2CommonLogic

Documentation

data Prop2CommonLogic Source #

lid of the morphism

Constructors

Prop2CommonLogic

Instances

Instances details

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