Data.Logic.Normal.Implicative

Documentation

type LiteralMapT f = StateT (Int, Map f Int)

type NormalT formula v term m a = SkolemT v term (LiteralMapT formula m) a

Combination of Normal monad and LiteralMap monad

runNormal :: NormalT formula v term Identity a -> a

runNormalT :: Monad m => NormalT formula v term m a -> m a

data ImplicativeForm lit

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.

Constructors

INF

Fields

neg :: Set lit

pos :: Set lit

Instances

Eq lit => Eq (ImplicativeForm lit)

(Data lit, Ord lit) => Data (ImplicativeForm lit)

Ord lit => Ord (ImplicativeForm lit)

Show lit => Show (ImplicativeForm lit)

makeINF' :: (Negatable lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit

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))

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

prettyINF :: (Negatable lit, Ord lit) => (lit -> Doc) -> ImplicativeForm lit -> Doc

prettyProof :: (Negatable lit, Ord lit) => (lit -> Doc) -> Set (ImplicativeForm lit) -> Doc