{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:18:20Z","timestamp":1725491900790},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730989"},{"type":"electronic","value":"9783540730996"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73099-6_18","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T07:04:02Z","timestamp":1189753442000},"page":"233-237","source":"Crossref","is-referenced-by-count":0,"title":["Improvements to the Tableau Prover PITP"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Avellone","sequence":"first","affiliation":[]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[]},{"given":"Ugo","family":"Moscato","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"18_CR1","first-page":"23","volume":"153","author":"A. Avellone","year":"2006","unstructured":"Avellone, A., Ferrari, M., Fiorentini, C., Fiorino, G., Moscato, U.: Esbc: an application for computing stabilization bounds. ENTCS\u00a0153(1), 23\u201333 (2006)","journal-title":"ENTCS"},{"key":"18_CR2","unstructured":"Avellone, A., Fiorino, G., Moscato, U.: A parallel implementation of a decision procedure for propositional intuitionistic logic. In: Mayer, M.C., Pirri, F. (eds.) TABLEAUX, POSITION PAPERS AND TUTORIALS (2003)"},{"key":"18_CR3","unstructured":"Avellone, A., Fiorino, G., Moscato, U.: A new O(n lg n)-space decision procedure for propositional intuitionistic logic. In: Baaz, A. V. M., Makowsky, J. (eds.), volume VIII of Kurt G\u00f6del Society, Collegium Logicum, pp. 17\u201333 (2004)"},{"key":"18_CR4","unstructured":"Avellone, A., Fiorino, G., Moscato, U.: A Tableau Decision Procedure for Propositional Intuitionistic Logic. In Proceedings of the 6th International Workshop on the Implementation of Logic, of CEUR Workshop Proceedings, vol. 212, pp. 64\u201379 (2006)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1007\/978-3-540-30124-0_37","volume-title":"Computer Science Logic","author":"A. Avellone","year":"2004","unstructured":"Avellone, A., Fiorentini, C., Fiorino, G., Moscato, U.: A space efficient implementation of a tableau calculus for a logic with a constructive negation. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 488\u2013502. Springer, Heidelberg (2004)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Avellone, A., Fiorino, G., Moscato, U.: Optimization techniques for propositional intuitionistic logic and their implementation. submitted to JAL (2007), http:\/\/www.dimequant.unimib.it\/PITP\/index.html","DOI":"10.1016\/j.tcs.2008.08.013"},{"volume-title":"Implementing Mathematics with the Nuprl Proof Development System","year":"1986","key":"18_CR7","unstructured":"Constable, R. (ed.): Implementing Mathematics with the Nuprl Proof Development System. Prentice\u2013Hall, Englewood Cliffs, New Jersey (1986)"},{"issue":"1-2","key":"18_CR8","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/FI-1999-391204","volume":"39","author":"U. Egly","year":"1999","unstructured":"Egly, U., Schmitt, S.: On intuitionistic proof transformations, their complexity, and application to constructive program synthesis. Fundam. Inform.\u00a039(1-2), 59\u201383 (1999)","journal-title":"Fundam. Inform."},{"key":"18_CR9","unstructured":"Fiorino, G.: Decision procedures for propositional intermediate logics. PhD thesis, Dipartimento di Scienze dell\u2019Informazione, Universita\u2019 degli Studi di Milano, Italy (2001)"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. Handbook of Automated Reasoning, pp. 100\u2013178. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"18_CR11","unstructured":"Horrocks, I.: Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester (1997)"},{"key":"18_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/3-540-45744-5_58","volume-title":"Automated Reasoning","author":"D. Larchey-Wendling","year":"2001","unstructured":"Larchey-Wendling, D., M\u00e9ry, D., Galmiche, D.: Strip: Structural sharing for efficient proof-search. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 696\u2013700. Springer, Heidelberg (2001)"},{"key":"18_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-69778-0_24","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"F. Massacci","year":"1998","unstructured":"Massacci, F.: Simplification: A general constraint propagation technique for propositional and modal tableaux. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 217\u2013232. Springer, Heidelberg (1998)"},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1008780817617","volume":"17","author":"M. Mendler","year":"2000","unstructured":"Mendler, M.: Timing analysis of combinational circuits in intuitionistic propositional logic. Formal Methods in System Design\u00a017(1), 5\u201337 (2000)","journal-title":"Formal Methods in System Design"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. release v1.1. To appear in JAR (2006)","DOI":"10.1007\/s10817-006-9060-z"},{"issue":"5","key":"18_CR16","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1992","unstructured":"Sahlin, D., Franz\u00e9n, T., Haridi, S.: An intuitionistic predicate logic theorem prover. J. Log. Comput.\u00a02(5), 619\u2013656 (1992)","journal-title":"J. Log. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T04:13:55Z","timestamp":1684037635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540730989","9783540730996"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}