<p>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?</p>
<p>I inquire because, from an intuitive perspective, logic programming languages such as Prolog appear to <em>directly</em> 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 &quot;recurrent&quot; (i.e. the model of computation and logic are the same entity)?</p>
<p>[0] <a href="https://en.wikipedia.org/wiki/Proof_procedure" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Proof_procedure</a></p>
<p>[1] <a href="https://en.wikipedia.org/wiki/Resolution_(logic)" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Resolution_(logic)</a></p>
<p>[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 href="https://arxiv.org/abs/2109.01483" rel="nofollow noreferrer">A Survey of the Proof-Theoretic Foundations of Logic Programming</a></p>

CC BY-SA 4.0
2022-06-17T20:02:12.543Z
Let's be clear: logic programing is *not* "propositions-as-programs" in any meaningful way; rather it's "proof search as programs".
cody
CC BY-SA 4.0
2022-06-19T03:12:01.013Z
@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?
jpt4
<lo.logic><typed-lambda-calculus><proof-theory><first-order-logic><curry-howard>
What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?
jpt4
# What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?

(Asked by: username_0 on 2022-06-11)

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](https://arxiv.org/abs/2109.01483)

**Tags:** lo.logic, typed-lambda-calculus, proof-theory, first-order-logic, curry-howard

> **Comments:**
> **username_1**: Let's be clear: logic programing is *not* "propositions-as-programs" in any meaningful way; rather it's "proof search as programs".  
> **username_0**: @username_1, 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?  

---

## 0 answers

