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.bro...@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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
