{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:27:42Z","timestamp":1743154062424,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230243"},{"type":"electronic","value":"9783540301240"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_37","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T12:27:59Z","timestamp":1267532879000},"page":"488-502","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Avellone","sequence":"first","affiliation":[]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[]},{"given":"Ugo","family":"Moscato","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"key":"37_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BFb0027403","volume-title":"Automated reasoning with analytic tableaux and related methods (Pont-\u2018a-Mousson, 1997)","author":"S. Akama","year":"1997","unstructured":"Akama, S.: Tableaux for logic programming with strong negation. In: Automated reasoning with analytic tableaux and related methods (Pont-\u2018a-Mousson, 1997). LNCS (LNAI), pp. 31\u201342. Springer, Berlin (1997)"},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"Avellone, A., Fiorentini, C., Fiorino, G., Moscato, U.: An efficient implementation of a tableau calculus for a logic with a constructive negation. Technical Report 83, Dipartimento di Metodi Quantitativi per le Scienze Economiche Aziendali, Universit\u00e1 Milano-Bicocca (2004) \n\nhttp:\/\/homes.dsi.unimi.it\/~fiorenti.\n\n\n (available at)","DOI":"10.1007\/978-3-540-30124-0_37"},{"key":"37_CR3","unstructured":"Benini, M.: Verification and Analysis of Programs in a Constructive Environment. PhD thesis, Dipartimento di Scienze dell\u2019Informazione, Universit\u2018a degli Studi di Milano, Italy (1999)"},{"issue":"3","key":"37_CR4","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic\u00a057(3), 795\u2013807 (1992)","journal-title":"Journal of Symbolic Logic"},{"key":"37_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/3-540-45607-4_14","volume-title":"Logic Based Program Synthesis and Transformation","author":"M. Ferrari","year":"2002","unstructured":"Ferrari, M., Fiorentini, C., Ornaghi, M.: Extracting exact time bounds from logical proofs. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol.\u00a02372, pp. 245\u2013265. Springer, Heidelberg (2002)"},{"issue":"6","key":"37_CR6","doi-asserted-by":"publisher","first-page":"955","DOI":"10.1093\/logcom\/12.6.955","volume":"12","author":"G. Fiorino","year":"2002","unstructured":"Fiorino, G.: Space-efficient decision procedures for three interpolable propositional intermediate logics. J. Logic Comput.\u00a012(6), 955\u2013992 (2002)","journal-title":"J. Logic Comput."},{"issue":"6","key":"37_CR7","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1093\/jigpal\/11.6.615","volume":"11","author":"I. Hasuo","year":"2003","unstructured":"Hasuo, I., Kashima, R.: Kripke completeness of first-order constructive logics with strong negation. IGPL\u00a011(6), 615\u2013646 (2003)","journal-title":"IGPL"},{"issue":"1","key":"37_CR8","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J. Hudelmaier","year":"1993","unstructured":"Hudelmaier, J.: An O(n log n)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation\u00a03(1), 63\u201375 (1993)","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"37_CR9","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1093\/jigpal\/5.1.145","volume":"5","author":"P. Miglioli","year":"1997","unstructured":"Miglioli, P., Moscato, U., Ornaghi, M.: Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic. Logic Journal of the IGPL\u00a05(1), 145\u2013167 (1997)","journal-title":"Logic Journal of the IGPL"},{"issue":"1","key":"37_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1305\/ndjfl\/1093634996","volume":"30","author":"P. Miglioli","year":"1989","unstructured":"Miglioli, P., Moscato, U., Ornaghi, M., Usberti, G.: A constructivism based on classical truth. Notre Dame J. Formal Logic\u00a030(1), 67\u201390 (1989)","journal-title":"Notre Dame J. Formal Logic"},{"key":"37_CR11","doi-asserted-by":"publisher","first-page":"16","DOI":"10.2307\/2268973","volume":"14","author":"D. Nelson","year":"1949","unstructured":"Nelson, D.: Constructible falsity. J. Symbolic Logic\u00a014, 16\u201326 (1949)","journal-title":"J. Symbolic Logic"},{"key":"37_CR12","series-title":"Lecture Notes in Comput. Sci","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/BFb0031924","volume-title":"Nonclassical logics and information processing (Berlin, 1990)","author":"D. Pearce","year":"1992","unstructured":"Pearce, D.: Reasoning with negative information. II. Hard negation, strong negation and logic programs. In: Nonclassical logics and information processing (Berlin, 1990). Lecture Notes in Comput. Sci, vol.\u00a0619, pp. 63\u201379. Springer, Berlin (1992)"},{"key":"37_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BFb0038700","volume-title":"Extensions of Logic Programming","author":"D. Pearce","year":"1991","unstructured":"Pearce, D., Wagner, G.: Logic programming with strong negation. In: Schroeder-Heister, P. (ed.) ELP 1989. LNCS, vol.\u00a0475, pp. 311\u2013326. Springer, Heidelberg (1991)"},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Thomason, R.H.: A semantical study of constructible falsity. In: Math, Z. (ed.) Logik Grundlagen Math., vol.\u00a015, pp. 247\u2013257 (1969)","DOI":"10.1002\/malq.19690151602"},{"key":"37_CR15","volume-title":"Basic Proof Theory, volume 43 of Cambridge Tracts in Theoretical Computer Science","author":"A.S. Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, volume 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1996)"},{"key":"37_CR16","first-page":"37","volume-title":"Sixteen papers on logic and algebra, volume 94 of American Mathematical Society Translations, Series 2","author":"N.N. Vorob\u00e9v","year":"1970","unstructured":"Vorob\u00e9v, N.N.: A new algorithm of derivability in a constructive calculus of statements. In: Sixteen papers on logic and algebra, volume 94 of American Mathematical Society Translations, Series 2, pp. 37\u201371. American Mathematical Society, Providence (1970)"},{"key":"37_CR17","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56734-8","volume-title":"The Logic of Information Structures","author":"H. Wansing","year":"1993","unstructured":"Wansing, H.: The Logic of Information Structures. LNCS (LNAI), vol.\u00a0681. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T20:03:58Z","timestamp":1579723438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}