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 ; 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 , 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)?
 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