{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,14]],"date-time":"2024-01-14T00:03:42Z","timestamp":1705190622792},"reference-count":22,"publisher":"World Scientific Pub Co Pte Ltd","issue":"02","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2004,4]]},"abstract":"<jats:p>In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs.<\/jats:p>","DOI":"10.1142\/s0129054104002509","type":"journal-article","created":{"date-parts":[[2004,4,22]],"date-time":"2004-04-22T13:19:46Z","timestamp":1082639986000},"page":"417-443","source":"Crossref","is-referenced-by-count":2,"title":["A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING"],"prefix":"10.1142","volume":"15","author":[{"given":"MANOLIS","family":"GERGATSOULIS","sequence":"first","affiliation":[{"name":"Department of Archive and Library Sciences, Ionian University, Palea Anaktora, Plateia Eleftherias, 49100 Corfu, Greece"}]},{"given":"CHRISTOS","family":"NOMIKOS","sequence":"additional","affiliation":[{"name":"Computer Science Department, University of Ioannina, Dourouti Campus, Ioannina, 451 10, Greece"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80070-7"},{"key":"rf2","first-page":"111","volume":"7","author":"Barringer H.","journal-title":"Formal Aspects of Computing"},{"key":"rf3","doi-asserted-by":"crossref","unstructured":"M.\u00a0Baudinet, Intensional Logics for Programming, eds. L.\u00a0Fari\u00f1as del Cerro and M.\u00a0Penttonen (Oxford University Press, 1993)\u00a0pp. 51\u201383.","DOI":"10.1093\/oso\/9780198537755.003.0003"},{"key":"rf4","unstructured":"M.\u00a0Baudinet, J.\u00a0Chomicki and P.\u00a0Wolper, Temporal Databases: Theory, Design, and Implementation, eds. L.\u00a0Fari\u00f1as del Cerro and M.\u00a0Penttonen (The Benjamin\/Cummings Publishing Company, Inc, 1993)\u00a0pp. 294\u2013320."},{"key":"rf6","doi-asserted-by":"publisher","DOI":"10.1080\/095281399146625"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00139-4"},{"key":"rf11","unstructured":"M.\u00a0Gergatsoulis, Encyclopedia of Microcomputers\u00a027, eds. A.\u00a0Kent and J. G.\u00a0Williams (Marcel Decker, Inc., 2001)\u00a0pp. 393\u2013408."},{"key":"rf13","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037535"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90016-A"},{"key":"rf15","unstructured":"C.\u00a0Liu and M.\u00a0Orgun, Intensional Programming I, ed. E. A.\u00a0Arhcroft (World-Scientific Publishing Company, Singapore, 1996)\u00a0pp. 281\u2013295."},{"key":"rf17","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0072"},{"key":"rf18","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00008-0"},{"key":"rf19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"rf20","unstructured":"A.\u00a0Montanary and B.\u00a0Pernici, Temporal Databases: Theory, Design, and Implementation, eds. L.\u00a0Fari\u00f1as del Cerro and M.\u00a0Penttonen (The Benjamin\/Cummings Publishing Company, Inc, 1993)\u00a0pp. 534\u2013562."},{"key":"rf22","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1996.tb00261.x"},{"key":"rf23","first-page":"1501","volume":"1","author":"Orgun M. A.","journal-title":"Journal of Computing and Information"},{"key":"rf24","first-page":"319","volume":"158","author":"Orgun M. A.","journal-title":"Theoretical Computer Science"},{"key":"rf26","doi-asserted-by":"crossref","unstructured":"M. A.\u00a0Orgun and W. W.\u00a0Wadge, Intensional Logics for Programming, eds. L.\u00a0Fari\u00f1as del Cerro and M.\u00a0Penttonen (Oxford University Press, 1992)\u00a0pp. 23\u201350.","DOI":"10.1093\/oso\/9780198537755.003.0002"},{"key":"rf31","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012502800961"},{"key":"rf33","doi-asserted-by":"publisher","DOI":"10.1016\/S0096-0551(98)00009-5"},{"key":"rf34","first-page":"733","volume":"33","author":"van Emden M. H.","journal-title":"J. ACM"},{"key":"rf35","doi-asserted-by":"crossref","first-page":"4","DOI":"10.3233\/AIC-1994-7102","volume":"7","author":"Vila L.","journal-title":"AI Communications"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054104002509","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,13]],"date-time":"2024-01-13T05:00:18Z","timestamp":1705122018000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054104002509"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4]]},"references-count":22,"journal-issue":{"issue":"02","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2004,4]]}},"alternative-id":["10.1142\/S0129054104002509"],"URL":"https:\/\/doi.org\/10.1142\/s0129054104002509","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4]]}}}