Copyright | (c) Till Mossakowski and Uni Bremen 2003 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | till@informatik.uni-bremen.de |
Stability | unstable |
Portability | non-portable |
Safe Haskell | None |
Assembles all the logics and comorphisms into a graph. The modules for the Grothendieck logic are logic graph indepdenent, and here is the logic graph that is used to instantiate these. Since the logic graph depends on a large number of modules for the individual logics, this separation of concerns (and possibility for separate compilation) is quite useful.
Comorphisms are either logic inclusions, or normal comorphisms. The former are assembled in inclusionList, the latter in normalList. An inclusion is an institution comorphism with the following properties:
- the signature translation is an embedding of categories
- the sentence translations are injective
- the model translations are isomorphisms
References:
The FLIRTS home page: http://www.informatik.uni-bremen.de/flirts
T. Mossakowski: Relating CASL with Other Specification Languages: the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.
Documentation
lookupSquare_in_LG :: AnyComorphism -> AnyComorphism -> Result [Square]