Re: [Haskell-cafe] Propositions in Haskell

[Patrick Browne]

The relation to theorem proving is the main motivation for my question.

In am trying to understand why some equations are ok and others not.

I suspect that in Haskell equations are definitions rather than assertions.

If approach 2 is a non-starter in Haskell, then can approach 1, using if-then-else, achieve the same results for propositions?

Thanks
Pat

On 15/05/13, Dan Mead <d.w.m...@gmail.com> wrote:

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

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