{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:08:01Z","timestamp":1725829681361},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_17","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"237-252","source":"Crossref","is-referenced-by-count":5,"title":["Proof-Search in Natural Deduction Calculus for Classical Propositional Logic"],"prefix":"10.1007","author":[{"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"17_CR1","unstructured":"Bolotov, A., Bocharov, V., Gorchakov, A., Shangin, V.: Automated first order natural deduction. In: Prasad, B. (ed.) IICAI, pp. 1292\u20131311. IICAI (2005)"},{"key":"17_CR2","unstructured":"D\u2019Agostino, M.: Classical natural deduction. In: Art\u00ebmov, S.N., et al. (eds.) We Will Show Them!, pp. 429\u2013468. College Publications (2005)"},{"issue":"1","key":"17_CR3","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/A:1005099619660","volume":"60","author":"R. Dyckhoff","year":"1998","unstructured":"Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Studia Logica\u00a060(1), 107\u2013118 (1998)","journal-title":"Studia Logica"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-40537-2_11","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Ferrari","year":"2013","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: A terminating evaluation-driven variant of g3i. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol.\u00a08123, pp. 104\u2013118. Springer, Heidelberg (2013)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: An evaluation-driven decision procedure for G3i. ACM Transactions on Computational Logic (TOCL), 6(1), 8:1\u20138:37 (2015)","DOI":"10.1145\/2660770"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Olivetti, N.: Goal-Directed Proof Theory. Springer (2000)","DOI":"10.1007\/978-94-017-1713-7"},{"key":"17_CR7","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and types. Camb. Univ. Press (1989)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Indrzejczak, A.: Natural Deduction, Hybrid Systems and Modal Logics. Trends in Logic, vol. 30. Springer (2010)","DOI":"10.1007\/978-90-481-8785-0"},{"key":"17_CR9","first-page":"5","volume":"1","author":"S. Ja\u015bkowski","year":"1934","unstructured":"Ja\u015bkowski, S.: On the rules of suppositions in formal logic. Studia Logica\u00a01, 5\u201332 (1934)","journal-title":"Studia Logica"},{"issue":"46","key":"17_CR10","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C. Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science\u00a0410(46), 4747\u20134768 (2009)","journal-title":"Theoretical Computer Science"},{"issue":"2-3","key":"17_CR11","first-page":"147","volume":"15","author":"D. Pastre","year":"2002","unstructured":"Pastre, D.: Strong and weak points of the MUSCADET theorem prover - examples from CASC-JC. AI Commun.\u00a015(2-3), 147\u2013160 (2002)","journal-title":"AI Commun."},{"key":"17_CR12","unstructured":"Pfenning, F.: Automated theorem proving. Lecture notes. CMU (2004)"},{"key":"17_CR13","unstructured":"Prawitz, D.: Natural Deduction. Almquist and Winksell (1965)"},{"issue":"1","key":"17_CR14","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1005091418752","volume":"60","author":"W. Sieg","year":"1998","unstructured":"Sieg, W., Byrnes, J.: Normal natural deduction proofs (in classical logic). Studia Logica\u00a060(1), 67\u2013106 (1998)","journal-title":"Studia Logica"},{"key":"17_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-32254-2_11","volume-title":"Mechanizing Mathematical Reasoning","author":"W. Sieg","year":"2005","unstructured":"Sieg, W., Cittadini, S.: Normal natural deduction proofs (in non-classical logics). In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol.\u00a02605, pp. 169\u2013191. Springer, Heidelberg (2005)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoretical Computer Science, vol.\u00a043. Camb. Univ. Press (2000)","DOI":"10.1017\/CBO9781139168717"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:59:25Z","timestamp":1559257165000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}