Hi,
Patrick Browne wrote:
In am trying to understand why some equations are ok and others not.
I suspect that in Haskell equations are definitions rather than assertions.
Yes. Haskell function definitions look like equations, but in many ways,
they aren't. Here is an example for an equation
I do understand the difference between theorem provers and Haskell programs.Logic can be used to reason 'about' Haskell programs and logic can be used 'within' Haskell programs.I am trying to clarify the difference between 'about' and 'within'Is approach 1 concerned with |= (model based
maybe this will help?
Haskell code in and of itself isn't special. proofs can happen with the
type system, but typically you'd want to define a target language and do
assertions about it, similar to how a compiler inspects it's input
programs. Haskell is not homoiconic nor is it like coq or
-- 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
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
Not exactly what you ask, but it is noteworthy that the mind has different
logic processors. The fastest one work with IF THEN ELSE rules applied
specifically to deals. This is why your example (and most examples of
logic) involves a kind of deal expressed in the first person. This trigger
a fast
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
You can stop suspecting: in Haskell, equations ARE definitions.
On May 15, 2013, at 9:15 PM, Patrick Browne patrick.bro...@dit.ie wrote:
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
Patrick Browne patrick.bro...@dit.ie writes:
-- Hi
By the way, this is unrelated to your actual question, but if you
haven't already, you might want to check out Bird-style Literate Haskell
so you don't have to put -- in front of all of your non-Haskell text
in a comment-heavy code-light file
