Comorphisms.hs revision fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3a
{- |
Module : $Id$
Description : various encodings
Copyright : (c) Uni Bremen 2005-2007
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable (existential types)
This folder contains various comorphisms (implemented using
the type class 'Logic.Comorphism.Comorphism'), which are then
collected to a logic graph in "Comorphisms.LogicGraph".
The latter is based on the list of logics collected in
The individual comorphisms are on the one hand trivial embeddings:
On the other hand, there are a number of real encodings:
"Comorphisms.CASL2PCFOL", "Comorphisms.CASL2TopSort" encodings of subsorting
"Comorphisms.CASL2SubCFOL" encoding of partiality
"Comorphisms.Sule2SoftFOL" translating a CASL subset to SoftFOL
"Comorphisms.Modal2CASL" encoding of Kripke worlds
translation of executable HasCASL subset to Haskell
unfinished coding of CSP-CASL LTS semantics as Kripke models
unfinished coding of CSP-CASL in IsabelleHOL
unfinished mapping of HasCASL subset to HasCASL program blocks
Finally, encodings to the theorem prover Isabelle:
unfinished translation of HasCASL subset to Isabelle
-}
module Comorphisms where