hets/Propositional/Tools.hs

	Tools.hs revision 926b3c5491f1c608f5b79e2d8014d7a1385558c3
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{-# OPTIONS -fallow-undecidable-instances #-}
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule      :  $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription :  Some additional helper functions
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederCopyright   :  (c) Dominik Luecke, Uni Bremen 2007
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer  :  luecke@tzi.de
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederStability   :  experimental
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability :  non-portable (imports Logic.Logic)
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederSome helper functions for Propositional Logic
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{-
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder  Ref.
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder  http://en.wikipedia.org/wiki/Propositional_logic
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder  What is a Logic?.
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder  In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder  2005.
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-}
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maedermodule Propositional.Tools
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder    (
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder     flatten                   -- "flattening" of specs
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder    ,flattenDis                -- "flattening" of disjunctions
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder    )
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder    where
ebcaad207cafc89eeb49d431f40de2ef4c48411cChristian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | the flatten functions use associtivity to "flatten" the syntax
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder-- | tree of the formulae
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | flatten \"flattens\" formulae under the assumption of the
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | semantics of basic specs, this means that we put each
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | \"clause\" into a single formula for CNF we really will obtain
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | clauses
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederflatten :: AS_BASIC.FORMULA -> [AS_BASIC.FORMULA]
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederflatten f =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder    case f of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder      AS_BASIC.Negation _ _       -> [f]
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder      AS_BASIC.Disjunction _ _    -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.Implication _ _ _  -> [f]
38775225cf810f5895cc03b4acbcfe8f84f2513aChristian Maeder      AS_BASIC.Equivalence _ _ _  -> [f]
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder      AS_BASIC.True_atom _        -> [f]
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder      AS_BASIC.False_atom _       -> [f]
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder      AS_BASIC.Predication _      -> [f]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder      AS_BASIC.Conjunction fs _   -> concat $ map flatten fs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder-- | "flattening" for disjunctions
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederflattenDis :: AS_BASIC.FORMULA -> [AS_BASIC.FORMULA]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederflattenDis f =
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder    case f of
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.Negation _ _       -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.Disjunction fs _   -> concat $ map flatten fs
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.Implication _ _ _  -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.Equivalence _ _ _  -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.True_atom _        -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.False_atom _       -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.Predication _      -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder      AS_BASIC.Conjunction _ _   -> [f]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder