{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:38:35Z","timestamp":1725489515538},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678953"},{"type":"electronic","value":"9783540446224"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44622-2_28","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T04:32:38Z","timestamp":1187238758000},"page":"411-426","source":"Crossref","is-referenced-by-count":8,"title":["Elimination of Negation in a Logical Framework"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Momigliano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,22]]},"reference":[{"unstructured":"D. P. A. Brogi, P. Mancarella and F. Turini. Universal quantification by case analysis. In Proc. ECAI-90, pages 111\u2013116, 1990.","key":"28_CR1"},{"key":"28_CR2","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1016\/0743-1066(94)90024-8","volume":"19","author":"K. Apt","year":"1994","unstructured":"K. Apt and R. Bol. Logic programming and negation. Journal of Logic Programming, 19\/20:9\u201372, May\/July 1994.","journal-title":"Journal of Logic Programming"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0743-1066(90)90023-X","volume":"8","author":"R. Barbuti","year":"1990","unstructured":"R. Barbuti, P. Mancarella, D. Pedreschi, and F. Turini. A transformational approach to negation in logic programming. Journal of Logic Programming, 8:201\u2013228, 1990.","journal-title":"Journal of Logic Programming"},{"unstructured":"A. Bonner. Hypothetical reasoning with intuitionistic logic. In R. Demolombe and T. Imielinski, editors, Non-Standard Queries and Answers, volume 306 of Studies in Logic and Computation, pages 187\u2013219. Oxford University Press, 1994.","key":"28_CR4"},{"key":"28_CR5","first-page":"293","volume-title":"Logic and Databases","author":"K. L. Clark","year":"1978","unstructured":"K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Databases, pages 293\u2013322. Plenum Press, New York, 1978."},{"issue":"4","key":"28_CR6","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0743-1066(85)80003-0","volume":"2","author":"D. M. Gabbay","year":"1985","unstructured":"D. M. Gabbay. N-Prolog: An extension of Prolog with hypothetical implications II. Logical foundations and negation as failure. Journal of Logic Programming, 2(4):251\u2013283, Dec. 1985.","journal-title":"Journal of Logic Programming"},{"issue":"2","key":"28_CR7","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/S0743-1066(97)10014-0","volume":"36","author":"L. Giordano","year":"1998","unstructured":"L. Giordano and N. Olivetti. Negation as failure and embedded implication. Journal of Logic Programming, 36(2):91\u2013147, August 1998.","journal-title":"Journal of Logic Programming"},{"unstructured":"J. Harland. On Hereditary Harrop Formulae as a Basis for Logic Programming. PhD thesis, Edinburgh, Jan. 1991.","key":"28_CR8"},{"issue":"1","key":"28_CR9","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, Jan. 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"28_CR10","first-page":"301","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"J.-L. Lassez and K. Marriot. Explicit representation of terms defined by counter examples. Journal of Automated Reasoning, 3(3):301\u2013318, Sept. 1987.","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In G. Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, pages 434\u2013445, Warsaw, Poland, June 1997.","key":"28_CR11","DOI":"10.1109\/LICS.1997.614968"},{"key":"28_CR12","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"},{"doi-asserted-by":"crossref","unstructured":"A. Momigliano. Elimination of Negation in a Logical Framework. PhD thesis, Carnegie Mellon University, 2000. Forthcoming.","key":"28_CR13","DOI":"10.1007\/3-540-44622-2_28"},{"unstructured":"A. Momigliano and F. Pfenning. The relative complement problem for higher-order patterns. In D. D. Schreye, editor, Proceedings of the 1999 International Conference on Logic Programming (ICLP\u201999), pages 389\u2013395, La Cruces, New Mexico, 1999. MIT Press.","key":"28_CR14"},{"unstructured":"G. Nadathur and D. Miller. An overview of \u03bbProlog. In K. A. Bowen and R. A Kowalski, editors, Fifth International Logic Programming Conference, pages 810\u2013827, Seattle, Washington, Aug. 1988. MIT Press.","key":"28_CR15"},{"doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logical frameworks. In A Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 2000. In preparation.","key":"28_CR16","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"unstructured":"T. Sato and H. Tamaki. Transformational logic program synthesis. In International Conference on Fifth Generation Computer Systems, 1984.","key":"28_CR17"},{"unstructured":"C. Sch\u00fcrmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, 2000. forthcoming.","key":"28_CR18"},{"key":"28_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/BFb0054266","volume-title":"Proceedings of the 15th International Conference on Automated Deduction (CADE-15)","author":"C. Sch\u00fcrmann","year":"1998","unstructured":"C. Sch\u00fcrmann and F. Pfenning. Automated theorem proving in a simple meta-logic for LF. In C. Kirchner and H. Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286\u2013300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44622-2_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T00:17:54Z","timestamp":1556756274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44622-2_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678953","9783540446224"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-44622-2_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}