Timeline for What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 19, 2022 at 3:24 | history | edited | jpt4 | CC BY-SA 4.0 |
Added new paper reference to investigate for possible answers.
|
| Jun 19, 2022 at 3:12 | comment | added | jpt4 | @cody, I agree that logic programming is not "propositions-as-programs". I write that "logic programming terms are exactly logical propositions, and programs directly manipulate such propositions", and inquire about what the computational correspondent of proof procedures might be. On the logic side, given propositions, a proof procedure manipulates them to yield a proof. Is it the case that "the algorithm that implements the manipulation of logical terms" is the computational correspondent? Thus, Robinson's Unification Algorithm is the computational correspondent to logical resolution? | |
| Jun 17, 2022 at 20:02 | comment | added | cody | Let's be clear: logic programing is not "propositions-as-programs" in any meaningful way; rather it's "proof search as programs". | |
| Jun 11, 2022 at 22:38 | history | asked | jpt4 | CC BY-SA 4.0 |