Logic_Propositional.hs revision 2af38fde95f93562f2124ec615fba0e509c8202e
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder{-# OPTIONS -fallow-undecidable-instances #-}
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederModule : $Header$
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederDescription : Instance of class Logic for propositional logic
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederMaintainer : luecke@tzi.de
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederStability : experimental
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederPortability : non-portable (imports Logic.Logic)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederInstance of class Logic for the propositional logic
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Also the instances for Syntax and Category.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder http://en.wikipedia.org/wiki/Propositional_logic
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder What is a Logic?.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhäuser.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder , Morphism) where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata Propositional = Propositional deriving Show --lid
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Language Propositional where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder description _ =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder "Propositional Logic\n\
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder \for more information please refer to\n\
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder \http://en.wikipedia.org/wiki/Propositional_logic"
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Category Propositional Sign Morphism where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder -- Identity morhpism
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder ide Propositional = idMor
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder -- Returns the domain of a morphism
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder dom Propositional = source
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder -- Returns the codomain of a morphism
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder cod Propositional = target
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder -- all sets are legal objects
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder legal_obj Propositional s = isLegalSignature s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder -- tests if the morphism is ok
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder legal_mor Propositional f = isLegalMorphism f
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder -- composition of morphisms
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder comp Propositional f g = composeMor f g
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Sentences Propositional Formula () Sign Morphism ()