Copyright | (c) Dominik Luecke, Uni Bremen 2007 |
---|---|

License | GPLv2 or higher, see LICENSE.txt |

Maintainer | luecke@informatik.uni-bremen.de |

Stability | experimental |

Portability | non-portable (imports Logic.Logic) |

Safe Haskell | Safe-Inferred |

Some helper functions for Propositional Logic

# Documentation

flatten :: FORMULA -> [FORMULA]

the flatten functions use associtivity to "flatten" the syntax tree of the formulae. flatten "flattens" formulae under the assumption of the semantics of basic specs, this means that we put each "clause" into a single formula for CNF we really will obtain clauses.

flattenDis :: FORMULA -> [FORMULA]

"flattening" for disjunctions