| Portability | portable |
|---|---|
| Stability | provisional |
| Maintainer | masahiro.sakai@gmail.com |
| Safe Haskell | Safe-Inferred |
Data.FOL.Formula
Description
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
Constructors
| 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) |
Instances
| 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