[Haskell-cafe] Propositions in Haskell

Dan Mead d.w.mead at gmail.com
Wed May 15 18:34:33 CEST 2013


i don't understand what you're trying to do with that code, however you
seem to be asking about theorem proving in general

check out

http://www.haskell.org/haskellwiki/Libraries_and_tools/Theorem_provers


and

http://en.wikipedia.org/wiki/Automated_theorem_proving


hope it helps


On Wed, May 15, 2013 at 11:34 AM, Patrick Browne <patrick.browne at dit.ie>wrote:

> -- Hi
> -- I am trying to show that a set of propositions and a conclusion the
> form a valid argument.
> -- I used two approaches; 1) using if-then-else, 2) using pattern matching.
> -- The version using if-then-else seems to be consistent with my knowledge
> of Haskell and logic (either of which could be wrong).
> -- Can the second approach be improved to better reflect the propositions
> and conclusion? Maybe type level reasoning could be used?
> --
> -- Valid argument?
> -- 1. I work hard or I play piano
> -- 2. If I work hard then I will get a bonus
> -- 3. But I did not get a bonus
> --     Therefore I played piano
> -- Variables: p = Piano, w = worked hard, b = got a bonus
> --    (w \/ p) /\ (w => b) /\ ¬(b)
> --   ---------------------------
> --                p
>
> -- First approach using language control structure if-then-else
> w, p, b::Bool
> -- Two equivalences for (w \/ p) as an implication.
> -- 1. (w \/ p) =equivalent-to=> (not p) => w
> -- 2. (w \/ p) =equivalent-to=> (not w) => p
> -- Picked 2
> p = if (not w) then True else False
> -- Contrapositive:  (w => b)  =equivalent-to=>  ~b => ~w
> w = if (not b) then False else True
> b = False
> -- gives p is true and w is false
>
> -- Second approach using pattern matching
> -- I think the rewriting goes from left to right but the logical inference
> goes in the opposite direction.
> w1, p1, b1::Bool
> p1 = (not w1)
> w1 = b1 -- Not consistent with statements, but I do not know how to write
> ~b1 => ~w1 in Haskell
> b1 = False
> -- Again gives p1 is true and w1 is false
>
>
> Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís
> Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a
> bheith slán. http://www.dit.ie
> This message has been scanned for content and viruses by the DIT
> Information Services E-Mail Scanning Service, and is believed to be clean.
> http://www.dit.ie
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130515/e3c14e8c/attachment.htm>


More information about the Haskell-Cafe mailing list