{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:32:41Z","timestamp":1726407161314},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_17","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T01:24:41Z","timestamp":1180661081000},"page":"254-268","source":"Crossref","is-referenced-by-count":0,"title":["Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"James","family":"Harland","sequence":"first","affiliation":[]},{"given":"Tatjana","family":"Lutovac","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Winikoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"J.-M. Andreoli. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation, 2(3), 1992.","DOI":"10.1093\/logcom\/2.3.297"},{"key":"17_CR2","unstructured":"J.-M. Andreoli and R. Pareschi. Linear Objects: Logical Processes with Built-in Inheritance. In David H. D. Warren and Peter Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 496\u2013510, Jerusalem, 1990. The MIT Press."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"K. Clark. Negation as Failure. In H. Gallaie and J. Minker, editors, Logic and Databases, pages 293\u2013323. Plenum Press, 1978.","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"R. Dyckhoff. Contraction-free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic, 57:795\u2013807, 1992.","journal-title":"Journal of Symbolic Logic"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1093\/jigpal\/7.3.319","volume":"7","author":"R. Dyckhoff","year":"1999","unstructured":"R. Dyckhoff. A Deterministic Terminating Sequent Calculus for Godel-Dummett logic. Logic Journal of the IGPL, 7:319\u2013326, 1999.","journal-title":"Logic Journal of the IGPL"},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(94)00105-7","volume":"135","author":"D. Galmiche","year":"1994","unstructured":"D. Galmiche and G. Perrier. On Proof Normalisation in Linear Logic. Theoretical Computer Science, 135:67\u2013110, 1994.","journal-title":"Theoretical Computer Science"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen. Untersuchungen \u00fciber das logische Schliessen. Math. Zeit., 39:176\u2013210,405-431, 1934.","journal-title":"Math. Zeit."},{"key":"17_CR8","unstructured":"J. Harland. On Normal Forms and Equivalence for Logic Programs. In Krzysztof Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 146\u2013160, Washington, DC, 1992. ALP, MIT Press."},{"issue":"1","key":"17_CR9","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1093\/logcom\/4.1.69","volume":"4","author":"J. Harland","year":"January1994","unstructured":"J. Harland. A Proof-Theoretic Analysis of Goal-Directed Provability. Journal of Logic and Computation, 4(1):69\u201388, January1994.","journal-title":"Journal of Logic and Computation"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/S0096-0551(97)00013-1","volume":"23","author":"J. Harland","year":"1997","unstructured":"J. Harland. On Goal-Directed Provability in Classical Logic. Computer Languages, 23:161\u2013178, 1997.","journal-title":"Computer Languages"},{"key":"17_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/BFb0014329","volume-title":"Programming in Lygon: An Overview","author":"J. Harland","year":"1996","unstructured":"J. Harland, D. Pym, and M. Winikoff. Programming in Lygon: An Overview. In M. Wirsing, editor, Lecture Notes in Computer Science, pages 391\u2013405. Springer, July1996."},{"issue":"2","key":"17_CR12","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J. Hodas","year":"1994","unstructured":"J. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation, 110(2):327\u2013365, 1994.","journal-title":"Information and Computation"},{"key":"17_CR13","unstructured":"N. Kobayash and A. Yonezawa. ACL-A Concurrent Linear Logic Programming Paradigm. In Dale Miller, editor, Logic Programming-Proceedings of the 1993 International Symposium, pages 279\u2013294, Vancouver, Canada, 1993. The MIT Press."},{"key":"17_CR14","unstructured":"T. Lutovac and J. Harland. Towards the Automation of the Design of Logic Programming Languages. Technical Report 97-30, Department of Computer Science, RMIT, 1997."},{"issue":"1","key":"17_CR15","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"D. Miller","year":"1996","unstructured":"D. Miller. Forum: A Multiple-Conclusion Specification Logic. Theoretical Computer Science, 165(1):201\u2013232, 1996.","journal-title":"Theoretical Computer Science"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logic, 51:125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"17_CR17","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0743-1066(90)90033-2","volume":"9","author":"J. Minker","year":"July1990","unstructured":"J. Minker and A. Rajasekar. A Fixpoint Semantics for Disjunctive Logic Programs. Journal of Logic Programming, 9(1):45\u201374, July1990.","journal-title":"Journal of Logic Programming"},{"issue":"2","key":"17_CR18","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1093\/logcom\/8.2.209","volume":"8","author":"G. Nadathur","year":"1998","unstructured":"G. Nadathur. Uniform Provability in Classical Logic. Journal of Logic and Computation, 8(2):209\u2013230, 1998.","journal-title":"Journal of Logic and Computation"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"D. Pym and J. Harland. A Uniform Proof-theoretic Investigation of Linear Logic Programming. Journal of Logic and Computation, 4(2): 175\u2013207, April1994.","DOI":"10.1093\/logcom\/4.2.175"},{"key":"17_CR20","unstructured":"E. Ritter, D. Pym, and L. Wallen. On the Intuitionistic Force of Classical Search, to appear in Theoretical Computer Science, 1999."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"P. Volpe. Concurrent Logic Programming as Uniform Linear Proofs. In G. Levi and M. Rodr\u00edguez-Artalejo, editors, Proceedings of the Conference on Algebraic and Logic Programming, pages 133\u2013149. Springer, 1994.","DOI":"10.1007\/3-540-58431-5_11"},{"key":"17_CR22","unstructured":"Lincoln Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990."},{"key":"17_CR23","unstructured":"M. Winikoff. Logic Programming with Linear Logic. PhD thesis, University of Melbourne, 1997."}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:24:10Z","timestamp":1556450650000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}