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

Safe HaskellNone

Data.Logic.Normal.Implicative

Synopsis

Documentation

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

Combination of Normal monad and LiteralMap monad

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 

Fields

neg :: Set lit
 
pos :: Set lit
 

Instances

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