Timeline for Does this Haskell code represent a decision procedure for a theorem?
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 16, 2020 at 10:30 | history | edited | CommunityBot |
Commonmark migration
|
|
| Dec 18, 2018 at 12:11 | history | edited | Patrick Browne | CC BY-SA 4.0 |
deleted 14 characters in body
|
| Dec 16, 2018 at 11:11 | history | edited | Patrick Browne | CC BY-SA 4.0 |
added 2 characters in body
|
| Dec 16, 2018 at 10:51 | history | edited | Patrick Browne | CC BY-SA 4.0 |
added 81 characters in body
|
| Dec 14, 2018 at 11:33 | history | edited | Patrick Browne | CC BY-SA 4.0 |
added 14 characters in body
|
| Dec 13, 2018 at 20:01 | history | edited | Patrick Browne | CC BY-SA 4.0 |
added 28 characters in body
|
| Dec 13, 2018 at 19:40 | history | edited | Patrick Browne | CC BY-SA 4.0 |
added 3 characters in body
|
| Dec 13, 2018 at 19:24 | history | edited | Patrick Browne | CC BY-SA 4.0 |
added 773 characters in body
|
| Dec 7, 2018 at 11:05 | comment | added | xuq01 | I have no doubts that the theorems are true. But you will want to prove if the output of your program satisfies your theory using either an automated theorem prover or a proof assistant. | |
| Dec 7, 2018 at 9:37 | history | edited | Patrick Browne | CC BY-SA 4.0 |
deleted 53 characters in body
|
| Dec 7, 2018 at 9:32 | comment | added | Patrick Browne | @xuq01 I have already used an automatic theorem prover to prove the theorems. | |
| Dec 7, 2018 at 9:29 | comment | added | Patrick Browne | @Derek Elkins Your comment identifies my confusion on the relation between a logical theory (in FOL) and Haskell program purporting to represent that theory. From my previous post on this topic the execution of a Haskell program does not count as a proof, from this post my code does not represent a decision procedure. | |
| Dec 7, 2018 at 9:23 | history | edited | Patrick Browne | CC BY-SA 4.0 |
added 405 characters in body
|
| Dec 7, 2018 at 9:10 | comment | added | Patrick Browne | @stewbasic If I omit the False equations the theorems will not run. So, the False equations are included for operational rather than purely logical reasons. | |
| Dec 6, 2018 at 22:02 | comment | added | Derek Elkins left SE | A decision procedure for a formula $\varphi$ (or, alternatively, set $S$) takes as input a term $x$ and outputs whether $\varphi(x)$ (or $x\in S$) holds. It doesn't make sense to ask if something is a decision procedure for a theorem. You are also adding a closed world assumption though that doesn't impact the particular statements presented as theorems. | |
| Dec 6, 2018 at 21:50 | comment | added | stewbasic |
In belongs (_,_) = False and lieOn (_,_) = False you seem to be assuming that a city can only belong to one country and only lie on one river. However all of the theorems can be proven without this assumption.
|
|
| Dec 6, 2018 at 21:08 | comment | added | xuq01 | I am tempted to say "prove it in Coq..." | |
| Dec 6, 2018 at 19:28 | history | asked | Patrick Browne | CC BY-SA 4.0 |