9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Some additional helper functions
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik LueckeCopyright : (c) Dominik Luecke, Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik LueckeStability : experimental
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik LueckePortability : non-portable (imports Logic.Logic)
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik LueckeSome helper functions for Propositional Logic
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik Luecke http://en.wikipedia.org/wiki/Propositional_logic
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik Luecke Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
1b5b696aa3bc2a6747a4eeac777f850788482c98Dominik Luecke What is a Logic?.
926b3c5491f1c608f5b79e2d8014d7a1385558c3Dominik Luecke In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
4f4af799873e53cd4cef76775afa22fdf94b6780Christian Maeder ( flatten -- "flattening" of specs
4f4af799873e53cd4cef76775afa22fdf94b6780Christian Maeder , flattenDis -- "flattening" of disjunctions
91e80ba1d3d89546a6cc48153eef4a30d816c246Christian Maeder{- | the flatten functions use associtivity to "flatten" the syntax
91e80ba1d3d89546a6cc48153eef4a30d816c246Christian Maedertree of the formulae.
91e80ba1d3d89546a6cc48153eef4a30d816c246Christian Maederflatten \"flattens\" formulae under the assumption of the
91e80ba1d3d89546a6cc48153eef4a30d816c246Christian Maedersemantics of basic specs, this means that we put each
91e80ba1d3d89546a6cc48153eef4a30d816c246Christian Maeder\"clause\" into a single formula for CNF we really will obtain
9ab0e17a1478d65b355987bc148e288844df3810Christian Maederflatten :: FORMULA -> [FORMULA]
4f4af799873e53cd4cef76775afa22fdf94b6780Christian Maederflatten f = case f of
9ab0e17a1478d65b355987bc148e288844df3810Christian Maeder Conjunction fs _ -> concatMap flatten fs
bdc3d22af3cfaeac7e9776a12371fe1d534ebcaeDominik Luecke-- | "flattening" for disjunctions
9ab0e17a1478d65b355987bc148e288844df3810Christian MaederflattenDis :: FORMULA -> [FORMULA]
4f4af799873e53cd4cef76775afa22fdf94b6780Christian MaederflattenDis f = case f of
9ab0e17a1478d65b355987bc148e288844df3810Christian Maeder Disjunction fs _ -> concatMap flattenDis fs