logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Data.Logic.Normal.Implicative

Synopsis

# Documentation

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

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

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.

Constructors

 INF Fieldsneg :: Set lit pos :: Set lit

Instances

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

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

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