Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski, and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (various -fglasgow-exts extensions)
Safe HaskellNone

Logic.Logic

Description

Central interface (type class) for logics in Hets

Provides data structures for logics (with symbols). Logics are a type class with an identity type (usually interpreted by a singleton set) which serves to treat logics as data. All the functions in the type class take the identity as first argument in order to determine the logic.

For logic (co)morphisms see Logic.Comorphism

This module uses multiparameter type classes with functional dependencies (http://www.haskell.org/haskellwiki/Functional_dependencies) for defining an interface for the notion of logic. Multiparameter type classes are needed because a logic consists of a collection of types, together with operations on these. Functional dependencies are needed because no operation will involve all types of the multiparameter type class; hence we need a method to derive the missing types. We chose an easy way: for each logic, we introduce a new singleton type that is the name, or constitutes the identity of the logic. All other types of the multiparameter type class depend on this identity constituting type, and all operations take the 'identity constituting' type as first arguments. The value of the argument of the identity constituting type is irrelevant (note that there is only one value of such a type anyway).

Note that we tend to use lid both for the identity type of a logic, as well as for its unique inhabitant, i.e. lid :: lid.

The other types involved in the definition of logic are as follows:

  • sign: signatures, that is, contexts, or non-logical vocabularies, typically consisting of a set of declared sorts, predicates, function symbols, propositional letters etc., together with their typing.
  • sentence: logical formulas.
  • basic_spec: abstract syntax of basic specifications. The latter are human-readable presentations of a signature together with some sentences.
  • symbol: symbols that may occur in a signature, fully qualified with their types
  • raw_symbol: symbols that may occur in a signature, possibly not or partially qualified
  • morphism: maps between signatures (typically preserving the structure).
  • symb_items: abstract syntax of symbol lists, used for declaring some symbols of a signature as hidden.
  • symb_map_items: abstract syntax of symbol maps, i.e. human-readable presentations of signature morphisms.
  • sublogics: sublogics of the given logic. This type might be a record of Boolean flags, indicating whether some feature is present in the sublogi of not.
  • proof_tree: proof trees.

References:

J. A. Goguen and R. M. Burstall Institutions: Abstract Model Theory for Specification and Programming JACM 39, p. 95-146, 1992 (general notion of logic - model theory only)

J. Meseguer General Logics Logic Colloquium 87, p. 275-329, North Holland, 1989 (general notion of logic - also proof theory; notion of logic representation, called map there)

T. Mossakowski: Specification in an arbitrary institution with symbols 14th WADT 1999, LNCS 1827, p. 252-270 (treatment of symbols and raw symbols, see also CASL semantics in the CASL reference manual)

T. Mossakowski, B. Klin: Institution Independent Static Analysis for CASL 15h WADT 2001, LNCS 2267, p. 221-237, 2002. (what is needed for static anaylsis)

S. Autexier and T. Mossakowski Integrating HOLCASL into the Development Graph Manager MAYA FroCoS 2002, LNCS 2309, p. 2-17, 2002. (interface to provers)

CoFI (ed.): CASL Reference Manual, LNCS 2960, Springer Verlag, 2004. (static semantics of CASL structured and architectural specifications)

T. Mossakowski Heterogeneous specification and the heterogeneous tool set Habilitation thesis, University of Bremen, 2005 (the general picture of heterogeneous specification)

Synopsis

Documentation

data Stability

Stability of logic implementations

class ShATermConvertible a => Convertible a

shortcut for class constraints

class (Pretty a, Convertible a) => PrintTypeConv a

shortcut for class constraints

Instances

class (Eq a, PrintTypeConv a) => EqPrintTypeConv a

shortcut for class constraints with equality

Instances

type EndoMap a = Map a a

maps from a to a

class Show lid => Language lid where

the name of a logic. Define instances like "data CASL = CASL deriving (Show, Typeable, Data)"

Minimal complete definition

Nothing

Methods

language_name :: lid -> String

description :: lid -> String

Instances

Language Isabelle 
Language HasCASL 
Language HolLight 
Language CSL 
Language Haskell 
Language CSMOF 
Language QVTR 
Language Adl 
Language OMDoc_PUN 
Language RelScheme 
Language Temporal

Instance of Language for temporal logic

Language DFOL 
Language LF 
Language FrameworkCom 
Language Framework 
Language Maude

Instance of Language for Maude

Language CommonLogic 
Language DMU 
Language RDF 
Language Grothendieck 
Language THF 
Language SoftFOL 
Language QBF 
Language OWL2 
Language Propositional 
Language THFP2THF0 
Language THFP_P2THFP 
Language THFP_P2HasCASL 
Language HasCASL2THFP_P 
Language HasCASL2HasCASL 
Language CommonLogic2IsabelleHOL 
Language HolLight2Isabelle 
Language HasCASL2IsabelleHOL 
Language PCoClTyConsHOL2IsabelleHOL 
Language MonadicHasCASL2IsabelleHOL 
Language PCoClTyConsHOL2PairsInIsaHOL 
Language HasCASL2PCoClTyConsHOL 
Language QBF2Prop 
Language Prop2QBF 
Language CommonLogicModuleElimination 
Language Prop2CommonLogic 
Language SoftFOL2CommonLogic 
Language DMU2OWL2 
Language OWL22CommonLogic 
Language Propositional2OWL2 
Language HasCASL2Haskell 
Language Haskell2IsabelleHOL 
Language Haskell2IsabelleHOLCF 
Language CASL 
Language CASL2PCFOL 
Language CASL2SubCFOL 
Language CASL2HasCASL 
Language CFOL2IsabelleHOL 
Language Prop2CASL 
Language CASL2Prop 
Language CASL2TopSort 
Language DFOL2CASL 
Language CSMOF2CASL 
Language QVTR2CASL 
Language RelScheme2CASL 
Language Maude2CASL 
Language CL2CFOL 
Language Adl2CASL 
Language OWL22CASL 
Language CASL2OWL 
Language Fpl 
Language Modal 
Language CASL2Modal 
Language Modal2CASL 
Language MODAL_EMBEDDING 
Language Hybrid 
Language CASL2Hybrid 
Language Hybrid2CASL 
Language ExtModal 
Language CASL2ExtModal 
Language ExtModal2CASL 
Language ExtModal2ExtModalNoSubsorts 
Language ExtModal2ExtModalTotal 
Language ExtModal2HasCASL 
Language ExtModal2OWL 
Language CoCASL 
Language CoCFOL2IsabelleHOL 
Language CoCASL2CoPCFOL 
Language CoCASL2CoSubCFOL 
Language CASL2CoCASL 
Language Hybridize 
Language CASL2CspCASL 
Language CspCASL2Modal 
Language COL 
Language CASL_DL 
Language CASL_DL2CASL 
Language ConstraintCASL 
Language VSE 
Language CASL2VSE 
Language CASL2VSERefine 
Language CASL2VSEImport 
Language FreeCAD 
Language lid => Language (IdModif lid) 
Language cid => Language (SpanDomain cid) 
Show a => Language (GenCspCASL a) 
(Language cid1, Language cid2) => Language (CompComorphism cid1 cid2) 
(Language lid, Eq sublogics, Show sublogics, SublogicName sublogics) => Language (InclComorphism lid sublogics) 
(Language lid1, Language lid2) => Language (HorCompModif lid1 lid2) 
(Language lid1, Language lid2) => Language (VerCompModif lid1 lid2) 
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree => Language (IdMorphism lid sublogics) 
(Show a, Show b) => Language (CspCASL2CspCASL a b) 

class (Ord object, Ord morphism) => Category object morphism | morphism -> object where

Categories are given as usual: objects, morphisms, identities, domain, codomain and composition. The type id is the name, or the identity of the category. It is an argument to all functions of the type class, serving disambiguation among instances (via the functional dependency lid -> object morphism). The types for objects and morphisms may be restricted to subtypes, using legal_obj and legal_mor. For example, for the category of sets and injective maps, legal_mor would check injectivity. Since Eq is a subclass of Category, it is also possible to impose a quotient on the types for objects and morphisms. Require Ord instances only for efficiency, i.e. in sets or maps.

Minimal complete definition

ide, composeMorphisms, dom, cod

Methods

ide :: object -> morphism

identity morphisms

composeMorphisms :: morphism -> morphism -> Result morphism

composition, in diagrammatic order, if intermediate objects are equal (not checked!)

dom, cod :: morphism -> object

domain and codomain of morphisms

inverse :: morphism -> Result morphism

the inverse of a morphism

isInclusion :: morphism -> Bool

test if the signature morphism an inclusion

legal_mor :: morphism -> Result ()

is a value of type morphism denoting a legal morphism?

Instances

Category Sign RDFMorphism 
Category Sign OWLMorphism 
Category Sign Morphism 
Category Sign Morphism

Instance of Category for Maude

Category Sign Morphism 
Category Sign Morphism 
Category Sign Morphism

Instance of Category for temporal logic

Category Sign RSMorphism

Instance of Category for Rel

Category Sign Morphism

Instance of Category for propositional logic

Category Sign Morphism

Instance of Category for propositional logic

Category Sign Morphism

Instance of Category for CSL logic

Category Env Morphism 
Category OMDoc_Sign OMDoc_Morphism 
Category Sgn_Wrap Mor 
Category G_sign GMorphism 
Ord sign => Category sign (DefaultMorphism sign) 
(Ord f, Ord e, Ord m, MorphismExtension e m) => Category (Sign f e) (Morphism f e m) 

isIdentity :: Category object morphism => morphism -> Bool

test if the signature morphism is the identity

comp :: Category object morphism => morphism -> morphism -> Result morphism

class (Language lid, PrintTypeConv basic_spec, GetRange basic_spec, Monoid basic_spec, Pretty symbol, EqPrintTypeConv symb_items, EqPrintTypeConv symb_map_items) => Syntax lid basic_spec symbol symb_items symb_map_items | lid -> basic_spec symbol symb_items symb_map_items where

Abstract syntax, parsing and printing. There are three types for abstract syntax: basic_spec is for basic specifications (see CASL RefMan p. 5ff.), symb_items is for symbol lists (see CASL RefMan p. 35ff.), symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).

Minimal complete definition

Nothing

Methods

parsersAndPrinters :: lid -> Map String (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)

parsers and printers

parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec)

parser for basic specifications

parseSingleSymbItem :: lid -> Maybe (AParser st symb_items)

parser for a single symbol returned as list

parse_symb_items :: lid -> Maybe (AParser st symb_items)

parser for symbol lists

parse_symb_map_items :: lid -> Maybe (AParser st symb_map_items)

parser for symbol maps

toItem :: lid -> basic_spec -> Item

Instances

Syntax Isabelle () () () () 
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems 
Syntax HolLight () () () () 
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS

Syntax of CSL logic

Syntax Haskell HsDecls Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax CSMOF Metamodel () () () 
Syntax QVTR Transformation () () () 
Syntax Adl Context Symbol () () 
Syntax OMDoc_PUN () Symbol () () 
Syntax RelScheme RSScheme RSSymbol () ()

Syntax of Rel

Syntax Temporal BASIC_SPEC Symbol () ()

Syntax of Temporal logic

Syntax DFOL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax LF BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax FrameworkCom ComorphismDef () () () 
Syntax Framework LogicDef () () () 
Syntax Maude MaudeText Symbol () ()

Instance of Syntax for Maude

Syntax CommonLogic BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax DMU Text () () () 
Syntax RDF TurtleDocument RDFEntity SymbItems SymbMapItems 
Syntax THF BasicSpecTHF SymbolTHF () () 
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS

Syntax of Propositional logic

Syntax OWL2 OntologyDocument Entity SymbItems SymbMapItems 
Syntax Propositional BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax CASL_DL DL_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax ConstraintCASL ConstraintCASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS 
Syntax FreeCAD Document () () () 
Syntax SoftFOL [TPTP] SFSymbol () () 
Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 => Syntax (SpanDomain cid) () sign_symbol1 () () 
Show a => Syntax (GenCspCASL a) CspBasicSpec CspSymbol CspSymbItems CspSymbMapItems

Syntax of CspCASL

basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)

basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (basic_spec -> Doc)

basicSpecSyntaxes :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> [String]

parserAndPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)

lookupDefault :: Syntax lid basic_spec symbol symb_items symb_map_items => lid -> Maybe IRI -> Map String b -> Maybe b

function to lookup parser or printer

showSyntax :: Language lid => lid -> Maybe IRI -> String

addSyntax :: String -> b -> Map String b -> Map String b

class (Language lid, Category sign morphism, Ord sentence, Ord symbol, PrintTypeConv sign, PrintTypeConv morphism, GetRange sentence, GetRange symbol, PrintTypeConv sentence, ToJson sentence, ToXml sentence, PrintTypeConv symbol) => Sentences lid sentence sign morphism symbol | lid -> sentence sign morphism symbol where

Sentences, provers and symbols. Provers capture the entailment relation between sets of sentences and sentences. They may return proof trees witnessing proofs. Signatures are equipped with underlying sets of symbols (such that the category of signatures becomes a concrete category), see CASL RefMan p. 191ff.

Minimal complete definition

Nothing

Methods

map_sen :: lid -> morphism -> sentence -> Result sentence

sentence translation along a signature morphism

simplify_sen :: lid -> sign -> sentence -> sentence

simplification of sentences (leave out qualifications)

negation :: lid -> sentence -> Maybe sentence

negation of a sentence for disproving

print_sign :: lid -> sign -> Doc

modified signature printing when followed by sentences

print_named :: lid -> Named sentence -> Doc

print a sentence with comments

sym_of :: lid -> sign -> [Set symbol]

dependency ordered list of symbol sets for a signature

mostSymsOf :: lid -> sign -> [symbol]

Dependency ordered list of a bigger symbol set for a signature. This function contains more symbols than those being subject to hiding and renaming (given by sym_of) to better represent a signature as a set of symbols given within xml files. At least for CASL additional symbols for (direct) subsorts will be created, but note, that no symbol for a partial function will be created, if the signature contains this function as total, although a signature with just that partial function would be a subsignature. This function is supposed to work over partial signatures created by signatureDiff.

symmap_of :: lid -> morphism -> EndoMap symbol

symbol map for a signature morphism

sym_name :: lid -> symbol -> Id

symbols have a name, see CASL RefMan p. 192

sym_label :: lid -> symbol -> Maybe String

some symbols have a label for better readability

fullSymName :: lid -> symbol -> String

the fully qualified name for XML output (i.e. of OWL2)

symKind :: lid -> symbol -> String

a logic dependent kind of a symbol

symsOfSen :: lid -> sentence -> [symbol]

the symbols occuring in a sentence (any order)

pair_symbols :: lid -> symbol -> symbol -> Result symbol

combine two symbols into another one

Instances

Sentences Isabelle Sentence Sign IsabelleMorphism () 
Sentences HasCASL Sentence Env Morphism Symbol 
Sentences HolLight Sentence Sign HolLightMorphism () 
Sentences CSL CMD Sign Morphism Symbol

Instance of Sentences for reduce logic

Sentences CSMOF Sen Sign Morphism () 
Sentences QVTR Sen Sign Morphism () 
Sentences Adl Sen Sign Morphism Symbol 
Sentences OMDoc_PUN () OMDoc_Sign OMDoc_Morphism Symbol 
Sentences RelScheme Sentence Sign RSMorphism RSSymbol

Instance of Sentences for Rel

Sentences Temporal FORMULA Sign Morphism Symbol

Instance of Sentences for temporal logic

Sentences DFOL FORMULA Sign Morphism Symbol 
Sentences LF Sentence Sign Morphism Symbol 
Sentences FrameworkCom () ComorphismDef MorphismCom () 
Sentences Framework () LogicDef Morphism () 
Sentences Maude Sentence Sign Morphism Symbol

Instance of Sentences for Maude

Sentences CommonLogic TEXT_META Sign Morphism Symbol 
Sentences RDF Axiom Sign RDFMorphism RDFEntity 
Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF 
Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol 
Sentences QBF FORMULA Sign Morphism Symbol

Instance of Sentences for propositional logic

Sentences OWL2 Axiom Sign OWLMorphism Entity 
Sentences Propositional FORMULA Sign Morphism Symbol

Instance of Sentences for propositional logic

Sentences CASL CASLFORMULA CASLSign CASLMor Symbol 
Sentences Fpl FplForm FplSign FplMor Symbol 
Sentences Modal ModalFORMULA MSign ModalMor Symbol 
Sentences Hybrid HybridFORMULA HSign HybridMor Symbol 
Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol 
Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol 
Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol 
Sentences COL COLFORMULA CSign COLMor Symbol 
Sentences CASL_DL DLFORMULA DLSign DLMor Symbol 
Sentences ConstraintCASL ConstraintCASLFORMULA ConstraintCASLSign ConstraintCASLMor Symbol 
Sentences VSE Sentence VSESign VSEMor Symbol 
Sentences FreeCAD () Sign FCMorphism () 
Sentences DMU () Text (DefaultMorphism Text) () 
Sentences Haskell (TiDecl PNT) Sign HaskellMorphism Symbol 
Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol

Instance of Sentences for CspCASL

Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 

singletonList :: a -> [a]

makes a singleton list from the given value

symset_of :: forall lid sentence sign morphism symbol. Sentences lid sentence sign morphism symbol => lid -> sign -> Set symbol

set of symbols for a signature

symlist_of :: forall lid sentence sign morphism symbol. Sentences lid sentence sign morphism symbol => lid -> sign -> [symbol]

dependency ordered list of symbols for a signature

inlineAxioms :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> String -> [Named sentence]

a dummy static analysis function to allow type checking *.inline.hs files

statFail :: (Language lid, Monad m) => lid -> String -> m a

fail function for static analysis

statError :: Language lid => lid -> String -> a

statErrMsg :: Language lid => lid -> String -> String

error message for static analysis

class (Syntax lid basic_spec symbol symb_items symb_map_items, Sentences lid sentence sign morphism symbol, GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol, Typeable raw_symbol) => StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol | lid -> basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol where

Minimal complete definition

empty_signature

Methods

basic_analysis :: lid -> Maybe ((basic_spec, sign, GlobalAnnos) -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))

static analysis of basic specifications and symbol maps. The resulting bspec has analyzed axioms in it. The resulting sign is an extension of the input sign plus newly declared or redeclared symbols. See CASL RefMan p. 138 ff.

sen_analysis :: lid -> Maybe ((basic_spec, sign, sentence) -> Result sentence)

Analysis of just sentences

extBasicAnalysis :: lid -> IRI -> LibName -> basic_spec -> sign -> GlobalAnnos -> Result (basic_spec, ExtSign sign symbol, [Named sentence])

a basic analysis with additional arguments

stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items] -> Result (EndoMap raw_symbol)

static analysis of symbol maps, see CASL RefMan p. 222f.

stat_symb_items :: lid -> sign -> [symb_items] -> Result [raw_symbol]

static analysis of symbol lists, see CASL RefMan p. 221f.

convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec)

convert a theory to basic specs for different serializations

ensures_amalgamability :: lid -> ([CASLAmalgOpt], Gr sign (Int, morphism), [(Int, morphism)], Gr String String) -> Result Amalgamates

architectural sharing analysis, see CASL RefMan p. 247ff.

quotient_term_algebra :: lid -> morphism -> [Named sentence] -> Result (sign, [Named sentence])

quotient term algebra for normalization of freeness

signature_colimit :: lid -> Gr sign (Int, morphism) -> Result (sign, Map Int morphism)

signature colimits

qualify :: lid -> SIMPLE_ID -> LibName -> morphism -> sign -> Result (morphism, [Named sentence])

rename and qualify the symbols considering a united incoming morphisms, code out overloading and create sentences for the overloading relation

symbol_to_raw :: lid -> symbol -> raw_symbol

Construe a symbol, like f:->t, as a raw symbol. This is a one-sided inverse to the function SymSySigSym in the CASL RefMan p. 192.

id_to_raw :: lid -> Id -> raw_symbol

Construe an identifier, like f, as a raw symbol. See CASL RefMan p. 192, function IDAsSym

matches :: lid -> symbol -> raw_symbol -> Bool

Check whether a symbol matches a raw symbol, for example, f:s->t matches f. See CASL RefMan p. 192

empty_signature :: lid -> sign

the empty (initial) signature, see CASL RefMan p. 193

add_symb_to_sign :: lid -> sign -> symbol -> Result sign

adds a symbol to a given signature

signature_union :: lid -> sign -> sign -> Result sign

union of signatures, see CASL RefMan p. 193

signatureDiff :: lid -> sign -> sign -> Result sign

difference of signatures resulting in unclosed pre-signatures

intersection :: lid -> sign -> sign -> Result sign

intersection of signatures

final_union :: lid -> sign -> sign -> Result sign

final union of signatures, see CASL RefMan p. 194

morphism_union :: lid -> morphism -> morphism -> Result morphism

union of signature morphims, see CASL RefMan p. 196

is_subsig :: lid -> sign -> sign -> Bool

subsignatures, see CASL RefMan p. 194

subsig_inclusion :: lid -> sign -> sign -> Result morphism

construct the inclusion morphisms between subsignatures, see CASL RefMan p. 194

generated_sign, cogenerated_sign :: lid -> Set symbol -> sign -> Result morphism

the signature (co)generated by a set of symbols in another signature is the smallest (largest) signature containing (excluding) the set of symbols. Needed for revealing and hiding, see CASL RefMan p. 197ff.

induced_from_morphism :: lid -> EndoMap raw_symbol -> sign -> Result morphism

Induce a signature morphism from a source signature and a raw symbol map. Needed for translation (SP with SM). See CASL RefMan p. 198

induced_from_to_morphism :: lid -> EndoMap raw_symbol -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism

Induce a signature morphism between two signatures by a raw symbol map. Needed for instantiation and views. See CASL RefMan p. 198f.

is_transportable :: lid -> morphism -> Bool

Check whether a signature morphism is transportable. See CASL RefMan p. 304f.

is_injective :: lid -> morphism -> Bool

Check whether the underlying symbol map of a signature morphism is injective

theory_to_taxonomy :: lid -> TaxoGraphKind -> MMiSSOntology -> sign -> [Named sentence] -> Result MMiSSOntology

generate an ontological taxonomy, if this makes sense

corresp2th :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> EndoMap symbol -> EndoMap symbol -> REL_REF -> Result (sign, [Named sentence], sign, sign, EndoMap symbol, EndoMap symbol)

create a theory from a correspondence

equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)

create a co-span fragment from an equivalence

Instances

StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol 
StaticAnalysis HolLight () Sentence () () Sign HolLightMorphism () ()

Static Analysis for propositional logic

StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol

Static Analysis for reduce logic

StaticAnalysis CSMOF Metamodel Sen () () Sign Morphism () () 
StaticAnalysis QVTR Transformation Sen () () Sign Morphism () () 
StaticAnalysis Adl Context Sen () () Sign Morphism Symbol RawSymbol 
StaticAnalysis OMDoc_PUN () () () () OMDoc_Sign OMDoc_Morphism Symbol () 
StaticAnalysis RelScheme RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol

Static Analysis for Rel

StaticAnalysis Temporal BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol

Static Analysis for propositional logic

StaticAnalysis DFOL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol 
StaticAnalysis LF BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM 
StaticAnalysis FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () 
StaticAnalysis Framework LogicDef () () () LogicDef Morphism () () 
StaticAnalysis Maude MaudeText Sentence () () Sign Morphism Symbol Symbol

Instance of StaticAnalysis for Maude

StaticAnalysis CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol 
StaticAnalysis RDF TurtleDocument Axiom SymbItems SymbMapItems Sign RDFMorphism RDFEntity RawSymb 
StaticAnalysis THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () 
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol

Static Analysis for propositional logic

StaticAnalysis OWL2 OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb 
StaticAnalysis Propositional BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol

Static Analysis for propositional logic

StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol 
StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol 
StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol 
StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol 
StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol 
StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol 
StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol 
StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol 
StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol 
StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol 
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol 
StaticAnalysis FreeCAD Document () () () Sign FCMorphism () () 
StaticAnalysis DMU Text () () () Text (DefaultMorphism Text) () () 
StaticAnalysis Haskell HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol 
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () 
Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol

Static Analysis for CspCASL

Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2 => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 

printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc

print a whole theory

inclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> sign -> sign -> Result morphism

guarded inclusion

class (Ord l, Show l) => SemiLatticeWithTop l where

semi lattices with top (needed for sublogics). Note that Ord is only used for efficiency and is not related to the partial order given by the lattice. Only Eq is used to define isSubElem

Methods

lub :: l -> l -> l

top :: l

isSubElem :: SemiLatticeWithTop l => l -> l -> Bool

less or equal for semi lattices

class MinSublogic sublogic item where

class providing the minimal sublogic of an item

Methods

minSublogic :: item -> sublogic

Instances

MinSublogic () a

a default instance for no sublogics

MinSublogic HolLightSL () 
MinSublogic HolLightSL Sign 
MinSublogic HolLightSL Sentence 
MinSublogic HolLightSL HolLightMorphism 
MinSublogic CASL_DL_SL SYMB_MAP_ITEMS 
MinSublogic CASL_DL_SL SYMB_ITEMS 
MinSublogic CASL_DL_SL Symbol 
MinSublogic CASL_DL_SL DL_BASIC_SPEC 
MinSublogic CASL_DL_SL DLSign 
MinSublogic CASL_DL_SL DLFORMULA 
MinSublogic CASL_DL_SL DLMor 
MinSublogic ProfSub Entity 
MinSublogic ProfSub SymbMapItems 
MinSublogic ProfSub SymbItems 
MinSublogic ProfSub Sign 
MinSublogic ProfSub OntologyDocument 
MinSublogic ProfSub Axiom 
MinSublogic ProfSub OWLMorphism 
MinSublogic CommonLogicSL Sign 
MinSublogic CommonLogicSL SYMB_ITEMS 
MinSublogic CommonLogicSL SYMB_MAP_ITEMS 
MinSublogic CommonLogicSL NAME 
MinSublogic CommonLogicSL TEXT_META 
MinSublogic CommonLogicSL BASIC_SPEC 
MinSublogic CommonLogicSL Morphism 
MinSublogic CommonLogicSL Symbol 
MinSublogic PropSL Sign 
MinSublogic PropSL SYMB_MAP_ITEMS 
MinSublogic PropSL SYMB_ITEMS 
MinSublogic PropSL FORMULA 
MinSublogic PropSL BASIC_SPEC 
MinSublogic PropSL Morphism 
MinSublogic PropSL Symbol 
MinSublogic QBFSL Sign 
MinSublogic QBFSL SYMBMAPITEMS 
MinSublogic QBFSL SYMBITEMS 
MinSublogic QBFSL FORMULA 
MinSublogic QBFSL BASICSPEC 
MinSublogic QBFSL Morphism 
MinSublogic QBFSL Symbol 
MinSublogic Sublogic SymbMapItems 
MinSublogic Sublogic SymbItems 
MinSublogic Sublogic BasicSpec 
MinSublogic Sublogic Symbol 
MinSublogic Sublogic Morphism 
MinSublogic Sublogic Env 
MinSublogic Sublogic Sentence 
MinSublogic THFSl () 
MinSublogic THFSl DefinedType 
MinSublogic THFSl THFUnaryConnective 
MinSublogic THFSl THFPairConnective 
MinSublogic THFSl Quantifier 
MinSublogic THFSl THFQuantifier 
MinSublogic THFSl THFSequent 
MinSublogic THFSl THFAtom 
MinSublogic THFSl THFBinaryType 
MinSublogic THFSl THFUnitaryType 
MinSublogic THFSl THFTopLevelType 
MinSublogic THFSl THFSubType 
MinSublogic THFSl THFTypeableFormula 
MinSublogic THFSl THFTypeFormula 
MinSublogic THFSl THFTypedConst 
MinSublogic THFSl THFVariable 
MinSublogic THFSl THFQuantifiedFormula 
MinSublogic THFSl THFUnitaryFormula 
MinSublogic THFSl THFBinaryTuple 
MinSublogic THFSl THFBinaryFormula 
MinSublogic THFSl THFLogicFormula 
MinSublogic THFSl THFFormula 
MinSublogic THFSl Kind 
MinSublogic THFSl Type 
MinSublogic THFSl SymbolTHF 
MinSublogic THFSl BasicSpecTHF 
MinSublogic THFSl SignTHF 
MinSublogic THFSl MorphismTHF 
Lattice a => MinSublogic (CASL_SL a) Symbol 
Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS 
Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS 
MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) 
MinSL a e => MinSublogic (CASL_SL a) (Sign f e) 
MinSL a e => MinSublogic (CASL_SL a) (Morphism f e m) 
(MinSL a f, MinSL a s, MinSL a b) => MinSublogic (CASL_SL a) (BASIC_SPEC b s f) 
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha 
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) 

type SyntaxTable = (PrecMap, AssocMap)

a type for syntax information eventually stored in the signature

class (StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol, SemiLatticeWithTop sublogics, MinSublogic sublogics sentence, ProjectSublogic sublogics basic_spec, ProjectSublogicM sublogics symb_items, ProjectSublogicM sublogics symb_map_items, ProjectSublogic sublogics sign, ProjectSublogic sublogics morphism, ProjectSublogicM sublogics symbol, Convertible sublogics, SublogicName sublogics, Ord proof_tree, Show proof_tree, Convertible proof_tree) => Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where

Minimal complete definition

Nothing

Methods

parse_basic_sen :: lid -> Maybe (basic_spec -> AParser st sentence)

stability :: lid -> Stability

stability of the implementation

data_logic :: lid -> Maybe AnyLogic

for a process logic, return its data logic

top_sublogic :: lid -> sublogics

the top sublogic, corresponding to the whole logic

all_sublogics :: lid -> [sublogics]

list all the sublogics of the current logic

bottomSublogic :: lid -> Maybe sublogics

sublogicDimensions :: lid -> [[sublogics]]

parseSublogic :: lid -> String -> Maybe sublogics

parse sublogic (override more efficiently)

proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism

provide the embedding of a projected signature into the original signature

provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]

several provers can be provided. See module Logic.Prover

cons_checkers :: lid -> [ConsChecker sign sentence sublogics morphism proof_tree]

consistency checkers

conservativityCheck :: lid -> [ConservativityChecker sign sentence morphism]

conservativity checkers

empty_proof_tree :: lid -> proof_tree

the empty proof tree

syntaxTable :: lid -> sign -> Maybe SyntaxTable

omdoc_metatheory :: lid -> Maybe OMCD

export_symToOmdoc :: lid -> NameMap symbol -> symbol -> String -> Result TCElement

export_senToOmdoc :: lid -> NameMap symbol -> sentence -> Result TCorOMElement

export_theoryToOmdoc :: lid -> SigMap symbol -> sign -> [Named sentence] -> Result [TCElement]

additional information which has to be exported can be exported by this function

omdocToSym :: lid -> SigMapI symbol -> TCElement -> String -> Result symbol

omdocToSen :: lid -> SigMapI symbol -> TCElement -> String -> Result (Maybe (Named sentence))

addOMadtToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [[OmdADT]] -> Result (sign, [Named sentence])

Algebraic Data Types are imported with this function. By default the input is returned without changes.

addOmdocToTheory :: lid -> SigMapI symbol -> (sign, [Named sentence]) -> [TCElement] -> Result (sign, [Named sentence])

additional information which has to be imported can be imported by this function. By default the input is returned without changes.

Instances

Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Logic HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () ()

Instance of Logic for propositional logc

Logic CSMOF () Metamodel Sen () () Sign Morphism () () () 
Logic QVTR () Transformation Sen () () Sign Morphism () () () 
Logic Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree 
Logic OMDoc_PUN () () () () () OMDoc_Sign OMDoc_Morphism Symbol () () 
Logic RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol ()

Instance of Logic for Relational Schemes

Logic Temporal () BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol ()

Instance of Logic for propositional logc

Logic DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () 
Logic LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () 
Logic FrameworkCom () ComorphismDef () () () ComorphismDef MorphismCom () () () 
Logic Framework () LogicDef () () () LogicDef Morphism () () () 
Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol ()

Instance of Logic for Maude

Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 
Logic RDF RDFSub TurtleDocument Axiom SymbItems SymbMapItems Sign RDFMorphism RDFEntity RawSymb ProofTree 
Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree 
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree

Instance of Logic for propositional logc

Logic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree 
Logic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree

Instance of Logic for propositional logc

Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree 
Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () 
Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () 
Logic Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () 
Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () 
Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () 
Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol () 
Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () 
Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree 
Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () 
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () 
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION]

Instance of Logic for reduce logc

Logic DMU () Text () () () Text (DefaultMorphism Text) () () () 
Logic FreeCAD () Document () () () Sign (DefaultMorphism Sign) () () () 
Logic Haskell Haskell_Sublogics HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol () 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree 
CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()

Instance of Logic for CspCASL

(MinSublogic sublogics1 (), Morphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 

class Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => LogicalFramework lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree | lid -> sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree where

Minimal complete definition

Nothing

Methods

base_sig :: lid -> sign

the base signature

write_logic :: lid -> String -> String

generation of the object logic instances second argument is object logic name

write_syntax :: lid -> String -> morphism -> String

generation of the Ltruth morphism declaration second argument is the object logic name third argument is the Ltruth morphism

write_proof :: lid -> String -> morphism -> String

write_model :: lid -> String -> morphism -> String

read_morphism :: lid -> FilePath -> morphism

write_comorphism :: lid -> String -> String -> String -> morphism -> morphism -> morphism -> String

emptyTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol => lid -> Theory sign sentence proof_tree

the empty theory

data AnyLogic

the disjoint union of all logics

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => Logic lid