{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T04:05:22Z","timestamp":1749873922392,"version":"3.41.0"},"reference-count":35,"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:\/\/www.springer.com\/tdm"}],"funder":[{"name":"JSPS Grant-in-Aid for Scientific Research","award":["(C) JP15K00305"],"award-info":[{"award-number":["(C) JP15K00305"]}]}],"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><jats:p>We consider some extensions of co-logic programming and study its relationship with the Horn<jats:inline-formula><jats:alternatives><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi mathvariant=\"italic\">\u03bc<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus by Charatonik et\u00a0al. We first consider<jats:italic>negation elimination (NE)<\/jats:italic>, a familiar technique of program transformation, for co-logic programs. Given a program<jats:italic>P<\/jats:italic>, NE derives its<jats:italic>dual<\/jats:italic>program<jats:inline-formula><jats:alternatives><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mi>P<\/mml:mi><mml:mo>*<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>which defines the \u201ccomplement\u201d of<jats:italic>P<\/jats:italic>. When we apply NE to co-logic programs with negation, we show that the stratification restriction, a syntactic condition imposed on co-logic programs, becomes too restrictive in general, and that the Horn<jats:inline-formula><jats:alternatives><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi mathvariant=\"italic\">\u03bc<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus can be used as an extension of co-logic programming for handling \u201cnon-stratified\u201d co-logic programs. We then consider some applications of non-stratified co-logic programs to the well-founded semantics (WFS) and Answer Set Programming. In particular, we give new iterated fixpoint characterizations of the WFS as well as answer sets via dual programs. We also discuss some applications of non-stratified co-logic programs to program transformation such as partial deduction, and a proof procedure for the WFS.<\/jats:p>","DOI":"10.1007\/s00165-016-0404-0","type":"journal-article","created":{"date-parts":[[2016,12,9]],"date-time":"2016-12-09T13:04:36Z","timestamp":1481288676000},"page":"401-421","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On dual programs in co-logic programming and the Horn \u03bc-calculus"],"prefix":"10.1145","volume":"29","author":[{"given":"Hirohisa","family":"Seki","sequence":"first","affiliation":[{"name":"Department of Computer Science, Nagoya Institute of Technology, 466-8555, Showa-ku, Nagoya, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03038308"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001960"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Apt KR (1990) Introduction to logic programming. In: Handbook of theoretical computer science Elsevier Amsterdam pp 493\u2013576","DOI":"10.1016\/B978-0-444-88074-1.50015-9"},{"volume-title":"Model checking","year":"1999","author":"Clarke EM","key":"e_1_2_1_2_4_2"},{"key":"e_1_2_1_2_5_2","unstructured":"Chan D (1988) Constructive negation based on the completed database. In: Proceeding of 5th international conference and symposium on logic programming MIT Press New York pp 111\u2013125"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Charatonik W McAllester D Niwinski D Podelski A Walukiewicz I (1998) The Horn Mu-calculus. In: LICS \u201998 IEEE Computer Society pp 58\u201369","DOI":"10.1109\/LICS.1998.705643"},{"key":"e_1_2_1_2_7_2","unstructured":"Colmerauer A (1982) Prolog and infinite trees. In: Clark KL Tarnlund SA (eds) Logic programming Academic Press New York pp 231\u2013251."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Chen W Warren DS (1993) Query evaluation under the well-founded semantics. In: Proceeding of the 12th ACM SIGACT-SIGMOD-SIGART symposium on principles of database systems PODS \u201993 pp 168\u2013179","DOI":"10.1145\/153850.153865"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Denecker M Bruynooghe M Vennekens J (2012) Approximation fixpoint theory and the semantics of logic and answers set programs. In: Correct reasoning volume 7265 of LNCS Springer New York pp 178\u2013194","DOI":"10.1007\/978-3-642-30743-0_13"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Farwer B (2002) \u03c9-automata. In: Automata logics and infinite games volume 2500 of LNCS Springer New York pp 3\u201321","DOI":"10.1007\/3-540-36387-4_1"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00330-3"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Gupta G Bansal A Min R Simon L Mallya A (2007) Coinductive logic programming and its applications. In: ICLP\u201907 volume 4670 of LNCS Springer New York pp 27\u201344","DOI":"10.1007\/978-3-540-74610-2_4"},{"key":"e_1_2_1_2_13_2","unstructured":"Gelfond M Lifschitz V (1988) The stable model semantics for logic programming. In: Proceeding of 5th international conference and symposium on logic programming MIT Press New York pp 1070\u20131080"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Gupta G Saeedloei N DeVries B Min R (2011) Infinite computation co-induction and computational logic. In: CALCO\u201911 Springer New York pp 40\u201354","DOI":"10.1007\/978-3-642-22944-2_4"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90027-7"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Jaffar J Stuckey P (1986) Semantics of infinite tree logic programming. http:\/\/www.utdallas.edu\/~gupta\/meta.html","DOI":"10.1016\/0304-3975(86)90027-7"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(91)90027-M"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Marple K Bansal A Min R Gupta G (2012) Goal-directed execution of answer set programs. In: PPDP\u201912 pp 35\u201344","DOI":"10.1145\/2370776.2370782"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000118"},{"key":"e_1_2_1_2_21_2","unstructured":"Min R (2010) Predicate answer set programming with coinduction. PhD thesis University of Texas at Dallas"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Przymusinski TC (1989) Every logic program has a natural stratification and an iterated least fixed point model. In: Proceedings of 8th ACM SIGMOD-SIGACT-SIGART symposium on principles of database systems pp 11\u201321","DOI":"10.1145\/73721.73723"},{"key":"e_1_2_1_2_23_2","unstructured":"Pereira LM Saptawijaya A (2012) Abductive logic programming with tabled abduction. In: Proceedings of ICSEA 2012 the 7th International conference on software engineering advances pp 548\u2013556"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Ross KA (1989) A procedural semantics for well founded negation in logic programs. In: Proceedings of 8th ACM SIGMOD-SIGACT-SIGART symposium on principles of database systems pp 22\u201333","DOI":"10.1145\/73721.73724"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Seki H (2012) Proving properties of co-logic programs by unfold\/fold transformations. In: LOPSTR\u201911 volume 7225 of LNCS pp 205\u2013220 Springer New York","DOI":"10.1007\/978-3-642-32211-2_14"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Seki H (2013) Proving properties of co-logic programs with negation by program transformations. In: LOPSTR\u201912 volume 7844 of LNCS pp 213\u2013227 Springer New York","DOI":"10.1007\/978-3-642-38197-3_14"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Seki H (2014) Extending co-logic programs for branching-time model checking. In: LOPSTR\u201913 volume 8901 of LNCS pp 127\u2013144. Springer New York","DOI":"10.1007\/978-3-319-14125-1_8"},{"key":"e_1_2_1_2_28_2","unstructured":"Seki H (2016) On dual programs in co-logic programming. In: LOPSTR\u201915 volume 9527 of LNCS pp 1\u201315 Springer New York"},{"key":"e_1_2_1_2_29_2","unstructured":"Simon LE (2006) Extending logic programming with coinduction. PhD thesis University of Texas at Dallas"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Simon L Mallya A Bansal A Gupta G (2006) Coinductive logic programming. In: ICLP\u201906 volume 4079 of LNCS pages 330\u2013344. Springer","DOI":"10.1007\/11799573_25"},{"key":"e_1_2_1_2_31_2","first-page":"4","article-title":"Tabled abduction in logic programs","volume":"13","author":"Saptawijaya A","year":"2013","journal-title":"Theor Pract Logic Program"},{"key":"e_1_2_1_2_32_2","unstructured":"Sato T Tamaki H (1984) Transformational logic program synthesis. In: FGCS\u201984 Tokyo pp 195\u2013201"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Van Gelder A (1989) The alternating fixpoint of logic programs with negation. In: Proceedings of 8th ACM SIGMOD-SIGACT-SIGART symposium on principles of database systems pp 1\u201310","DOI":"10.1145\/73721.73722"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Van Gelder A Ross K Schlipf JS (1988) Unfounded sets and well-founded semantics for general logic programs. In: Proceeding of 7th ACM SIGMOD-SIGACT-SIGART symposium on principles of database systems pp 211\u2013230","DOI":"10.1145\/308386.308444"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000494"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0404-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0404-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0404-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0404-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T11:34:37Z","timestamp":1749814477000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0404-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["10.1007\/s00165-016-0404-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0404-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,5]]}}}