{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T09:49:03Z","timestamp":1780566543116,"version":"3.54.1"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,1]],"date-time":"2017-05-01T00:00:00Z","timestamp":1493596800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K031864\/1-2"],"award-info":[{"award-number":["EP\/K031864\/1-2"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper presents a study of operational and type-theoretic properties of different resolution strategies in Horn clause logic. We distinguish four different kinds of resolution: resolution by unification (SLD-resolution), resolution by term-matching, the recently introduced structural resolution, and partial (or lazy) resolution. We express them all uniformly as abstract reduction systems, which allows us to undertake a thorough comparative analysis of their properties. To match this small-step semantics, we propose to take Howard\u2019s System\n            <jats:bold>H<\/jats:bold>\n            as a type-theoretic semantic counterpart. Using System\n            <jats:bold>H<\/jats:bold>\n            , we interpret Horn formulas as types, and a derivation for a given formula as the proof term inhabiting the type given by the formula. We prove soundness of these abstract reduction systems relative to System\n            <jats:bold>H<\/jats:bold>\n            , and we show completeness of SLD-resolution and structural resolution relative to System\n            <jats:bold>H<\/jats:bold>\n            . We identify conditions under which structural resolution is operationally equivalent to SLD-resolution. We show correspondence between term-matching resolution for Horn clause programs without existential variables and term rewriting.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0403-1","type":"journal-article","created":{"date-parts":[[2016,11,25]],"date-time":"2016-11-25T13:42:20Z","timestamp":1480081340000},"page":"453-474","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Operational semantics of resolution and productivity in Horn clause logic"],"prefix":"10.1145","volume":"29","author":[{"given":"Peng","family":"Fu","sequence":"first","affiliation":[{"name":"Heriot-Watt University, Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3240-0987","authenticated-orcid":false,"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_2_1_2_2_2","unstructured":"BarendregtHP (1992) Lambda calculiwith types. In:Abramsky S GabbayD Maibaum S (eds) Handbook of logic in computer science (vol. 2): background: computational structures. Oxford University Press Inc. New York pp 117\u2013309"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/280474"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Fu P Komendantskaya E Schrijvers T Pond A (2016) Proof relevant corecursive resolution. In: Functional and logic programming - 13th international symposium FLOPS 2016 Kochi Japan 4\u20136 March 2016 proceedings pp 126\u2013143","DOI":"10.1007\/978-3-319-29604-3_9"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Gupta G Bansal A Min R Simon L Mallya A (2007) Coinductive logic programming and its applications. In: Logic programming Springer New York pp 27\u201344","DOI":"10.1007\/978-3-540-74610-2_4"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/64805"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"e_1_2_1_2_8_2","unstructured":"Howard W (1980) The formulae-as-types notion of construction. In: Seldin J Hindley J (eds) To H. B. Curry: essays on combinatory logic lambda calculus and formalism Academic Press New York pp 479\u2013490"},{"key":"e_1_2_1_2_9_2","unstructured":"Jones SP Jones M Meijer E (1997) Type classes: an exploration of the design space. In: Haskell Workshop"},{"key":"e_1_2_1_2_10_2","unstructured":"Johann P Komendantskaya E Komendantskiy V (2015) Structural resolution for logic programming. In Technical Communications ICLP"},{"key":"e_1_2_1_2_11_2","unstructured":"Komendantskaya E Johann P (2015) Structural resolution: a framework for coinductive proof search and proof construction in horn clause logic. In: ACM Transactions on Computational Logic submitted"},{"key":"e_1_2_1_2_12_2","unstructured":"Komendantskaya E Johann P Schmidt M (2016) A productivity checker for logic programming. On-line Pre-Proceedings\nof LOPSTR\u201916 \u201c26th International Symposium on Logic-Based Program Synthesis and Transformation\u201d Edinburgh UK.\nhttps:\/\/arxiv.org\/abs\/1608.02534"},{"key":"e_1_2_1_2_13_2","unstructured":"Kleene SC (1980) Introduction to metamathematics 8th edn. North-Holland Publishing Company 1952. Co-publisher Wolters\u2013Noordhoff"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Komendantskaya E Power J (2011) Coalgebraic derivations in logic programming. In: CSL pp 352\u2013366","DOI":"10.1007\/978-3-642-22944-2_19"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Komendantskaya E Power J SchmidtM(2016) Coalgebraic logic programming: from semantics to implementation. J Logic\nComput 26(2):745\u2013783","DOI":"10.1093\/logcom\/exu026"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/39279"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"L\u00e4mmel R Peyton-Jones S (2005) Scrap your boilerplate with class: Extensible generic functions. In: Proceedings of 10th ACM SIGPLAN international conference on functional programming ICFP \u201905 pp 204\u2013215 New York NY USA ACM","DOI":"10.1145\/1086365.1086391"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Miller D Nadathur G Pfenning F Scedrov A (1991) Uniform proofs as a foundation for logic programming. Ann Pure Appl\nLogic 51(1\u20132):125\u2013157","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"e_1_2_1_2_19_2","unstructured":"Nilsson U Ma\u0142uszy\u0144ski J (1990) Logic programming and prolog. Wiley Chichester"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Pfenning F Sch\u00fcrmann C (1999) System description: Twelfa meta-logical framework for deductive systems. In: Automated deduction CADE-16 pp 202\u2013206 Springer New York","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Simon L Bansal A Mallya A Gupta G (2007) Co-logic programming: extending logic programming with coinduction. In: Automata languages and programming Springer New York pp 472\u2013483","DOI":"10.1007\/978-3-540-73420-8_42"},{"key":"e_1_2_1_2_22_2","volume-title":"Term rewriting systems","author":"Terese H","year":"2003"},{"key":"e_1_2_1_2_23_2","unstructured":"Zhou N-F Fruhman J (2013) A user guide to Picat. Available from http:\/\/picat-lang.org. Accessed 15 Nov 2016"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/2851529"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0403-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0403-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0403-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0403-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:56:52Z","timestamp":1641538612000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0403-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["10.1007\/s00165-016-0403-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0403-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5]]}}}