Portability | portable |
---|---|

Stability | provisional |

Maintainer | masahiro.sakai@gmail.com |

Safe Haskell | Safe-Inferred |

Formula of first order logic.

- module Algebra.Lattice.Boolean
- data Formula a
- pushNot :: Complement a => Formula a -> Formula a

# Overloaded operations for formula.

module Algebra.Lattice.Boolean

# Concrete formula

formulas of first order logic

T | |

F | |

Atom a | |

And (Formula a) (Formula a) | |

Or (Formula a) (Formula a) | |

Not (Formula a) | |

Imply (Formula a) (Formula a) | |

Equiv (Formula a) (Formula a) | |

Forall Var (Formula a) | |

Exists Var (Formula a) |

Eq a => Eq (Formula a) | |

Ord a => Ord (Formula a) | |

Show a => Show (Formula a) | |

JoinSemiLattice (Formula c) | |

MeetSemiLattice (Formula c) | |

Lattice (Formula c) | |

BoundedJoinSemiLattice (Formula c) | |

BoundedMeetSemiLattice (Formula c) | |

BoundedLattice (Formula c) | |

Variables a => Variables (Formula a) | |

Boolean (Formula c) | |

Complement (Formula a) | |

IsRel (Expr c) (Formula (Atom c)) |

pushNot :: Complement a => Formula a -> Formula aSource

convert a formula into negation normal form