1
$\begingroup$

The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed lambda calculus (computation side). To produce a proof, the proof calculus must be equipped with a proof procedure [0]; to produce a normalized type, the type system must be equipped with a type inference algorithm. What is the model of computation which corresponds to the rule of logical resolution [1], as is used in, e.g., Prolog? What is the computation side equivalent of the proof search procedure used to produce the resolvents of a resolution-based proof calculus?

I inquire because, from an intuitive perspective, logic programming languages such as Prolog appear to directly instantiate the logic side of the Correspondence. Types can be satisfied by multiple terms, and thus multiple programs can prove the same logical proposition. However, logic programming terms are exactly logical propositions, and programs directly manipulate such propositions. Is it the case that Correspondence is one-sided for resolution-based systems? Is the Correspondence for resolution "recurrent" (i.e. the model of computation and logic are the same entity)?

[0] https://en.wikipedia.org/wiki/Proof_procedure

[1] https://en.wikipedia.org/wiki/Resolution_(logic)

[20220618] Edit: This paper looks promising as far as an answer to this question is concerned, and I will update further after I have read it: A Survey of the Proof-Theoretic Foundations of Logic Programming

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ Let's be clear: logic programing is not "propositions-as-programs" in any meaningful way; rather it's "proof search as programs". $\endgroup$
    – cody
    Commented Jun 17, 2022 at 20:02
  • $\begingroup$ @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? $\endgroup$
    – jpt4
    Commented Jun 19, 2022 at 3:12

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.