Htaut.Theorem.Basic

Documentation

syllogism :: (Prop p, Prop q, Prop r) => Prove ((p -> q) -> (q -> r) -> p -> r)

syllogism' :: (Prop p, Prop q, Prop r) => Prove ((q -> r) -> (p -> q) -> p -> r)

propagate :: (Prop p, Prop q) => Prove (p -> (p -> q) -> q)

conditionSeperate :: (Prop p, Prop q, Prop r) => Prove ((p -> q -> r) -> (p -> q) -> p -> r)

conditionCommute :: (Prop p, Prop q, Prop r) => Prove ((p -> q -> r) -> q -> p -> r)

identity :: Prop p => Prove (p -> p)

conditionAdd :: (Prop p, Prop q) => Prove (q -> p -> q)

dunsScotus :: (Prop p, Prop q) => Prove (Neg p -> p -> q)

dunsScotus' :: (Prop p, Prop q) => Prove (p -> Neg p -> Neg q)