Skip to main content
Computer Science

Return to Question

added 19 characters in body
Source Link
Борат Сагдиев
Борат Сагдиев
  • 49
  • 6

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:

and [n*(n+1)/2 == sum [0..n] | n <- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems involving integers in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.

There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:

and [n*(n+1)/2 == sum [0..n] | n <- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.

There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:

and [n*(n+1)/2 == sum [0..n] | n <- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems involving integers in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.

There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.

Source Link
Борат Сагдиев
Борат Сагдиев
  • 49
  • 6

Prove simple theorems in Haskell in automated way

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:

and [n*(n+1)/2 == sum [0..n] | n <- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.

There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.