Safe Haskell | None |
---|
- type LiteralMapT f = StateT (Int, Map f Int)
- type NormalT formula v term m a = SkolemT v term (LiteralMapT formula m) a
- runNormal :: NormalT formula v term Identity a -> a
- runNormalT :: Monad m => NormalT formula v term m a -> m a
- data ImplicativeForm lit = INF {}
- makeINF' :: (Negatable lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit
- implicativeNormalForm :: forall m formula atom term v f lit. (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, Literal lit atom, Term term v f, Data formula, Ord formula, Ord lit, Data lit, Skolem f v) => formula -> SkolemT v term m (Set (ImplicativeForm lit))
- prettyINF :: (Negatable lit, Ord lit) => (lit -> Doc) -> ImplicativeForm lit -> Doc
- prettyProof :: (Negatable lit, Ord lit) => (lit -> Doc) -> Set (ImplicativeForm lit) -> Doc
Documentation
type NormalT formula v term m a = SkolemT v term (LiteralMapT formula m) aSource
Combination of Normal monad and LiteralMap monad
runNormalT :: Monad m => NormalT formula v term m a -> m aSource
data ImplicativeForm lit Source
A type to represent a formula in Implicative Normal Form. Such a
formula has the form a & b & c .=>. d | e | f
, where a thru f are
literals. One more restriction that is not implied by the type is
that no literal can appear in both the pos set and the neg set.
Typeable1 ImplicativeForm | |
Eq lit => Eq (ImplicativeForm lit) | |
(Typeable (ImplicativeForm lit), Data lit, Ord lit) => Data (ImplicativeForm lit) | |
(Eq (ImplicativeForm lit), Ord lit) => Ord (ImplicativeForm lit) | |
Show lit => Show (ImplicativeForm lit) |
makeINF' :: (Negatable lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm litSource
A version of MakeINF that takes lists instead of sets, used for implementing a more attractive show method.
implicativeNormalForm :: forall m formula atom term v f lit. (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, Literal lit atom, Term term v f, Data formula, Ord formula, Ord lit, Data lit, Skolem f v) => formula -> SkolemT v term m (Set (ImplicativeForm lit))Source
Take the clause normal form, and turn it into implicative form,
where each clauses becomes an (LHS, RHS) pair with the negated
literals on the LHS and the non-negated literals on the RHS:
(a | ~b | c | ~d) becomes (b & d) => (a | c)
(~b | ~d) | (a | c)
~~(~b | ~d) | (a | c)
~(b & d) | (a | c)
If there are skolem functions on the RHS, split the formula using
this identity:
(a | b | c) => (d & e & f)
becomes
a | b | c => d
a | b | c => e
a | b | c => f
prettyProof :: (Negatable lit, Ord lit) => (lit -> Doc) -> Set (ImplicativeForm lit) -> DocSource