{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,20]],"date-time":"2025-09-20T20:21:29Z","timestamp":1758399689788,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_20","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"293-301","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["System Description: GAPT 2.0"],"prefix":"10.1007","author":[{"given":"Gabriel","family":"Ebner","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[]},{"given":"Giselle","family":"Reis","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Riener","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Wolfsteiner","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Zivota","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"issue":"3","key":"20_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"PB Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in type theory. J. Symbolic Log. 36(3), 414\u2013432 (1971). doi:\n                      10.2307\/2269949","journal-title":"J. Symbolic Log."},{"issue":"2\u20133","key":"20_CR2","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/j.tcs.2008.02.043","volume":"403","author":"M Baaz","year":"2008","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: an analysis of f\u00fcrstenberg\u2019s proof of the infinity of primes. Theoret. Comput. Sci. 403(2\u20133), 160\u2013175 (2008)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"20_CR3","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/jsco.1999.0359","volume":"29","author":"M Baaz","year":"2000","unstructured":"Baaz, M., Leitsch, A.: Cut-elimination and redundancy-elimination by resolution. J. Symbolic Comput. 29(2), 149\u2013176 (2000)","journal-title":"J. Symbolic Comput."},{"key":"20_CR4","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \n                      \n                        \n                      \n                      $$\\lambda {\\Pi }$$\n                    -calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28\u201343 (2012)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., Paleo, B.W.: PROOFTOOL: a GUI for the GAPT framework. In: Kaliszyk, C., L\u00fcth, C. (eds.) Proceedings 10th International Workshop on User Interfaces for Theorem Provers (UITP) 2012, EPTCS, vol. 118, pp. 1\u201314 (2012)","DOI":"10.4204\/EPTCS.118.1"},{"issue":"6","key":"20_CR6","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1016\/j.apal.2015.01.002","volume":"166","author":"S Eberhard","year":"2015","unstructured":"Eberhard, S., Hetzl, S.: Inductive theorem proving based on tree grammars. Ann. Pure Appl. Log. 166(6), 665\u2013700 (2015)","journal-title":"Ann. Pure Appl. Log."},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-642-31374-5_32","volume-title":"Intelligent Computer Mathematics","author":"S Hetzl","year":"2012","unstructured":"Hetzl, S.: Project presentation: algorithmic structuring and compression of proofs (ASCOP). In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 438\u2013442. Springer, Heidelberg (2012)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/978-3-319-08587-6_17","volume-title":"Automated Reasoning","author":"S Hetzl","year":"2014","unstructured":"Hetzl, S., Leitsch, A., Reis, G., Tapolczai, J., Weller, D.: Introducing quantified cuts in logic with equality. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 240\u2013254. Springer, Heidelberg (2014)"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2014.05.018","volume":"549","author":"S Hetzl","year":"2014","unstructured":"Hetzl, S., Leitsch, A., Reis, G., Weller, D.: Algorithmic introduction of quantified cuts. Theoret. Comput. Sci. 549, 1\u201316 (2014)","journal-title":"Theoret. Comput. Sci."},{"issue":"12","key":"20_CR10","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1016\/j.apal.2011.06.005","volume":"162","author":"S Hetzl","year":"2011","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: CERES in higher-order logic. Ann. Pure Appl. Log. 162(12), 1001\u20131034 (2011)","journal-title":"Ann. Pure Appl. Log."},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-28717-6_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Hetzl","year":"2012","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 228\u2013242. Springer, Heidelberg (2012)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-40537-2_15","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S Hetzl","year":"2013","unstructured":"Hetzl, S., Libal, T., Riener, M., Rukhaia, M.: Understanding resolution proofs through Herbrand\u2019s theorem. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 157\u2013171. Springer, Heidelberg (2013)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-20398-5_14","volume-title":"NASA Formal Methods","author":"J Hurd","year":"2011","unstructured":"Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177\u2013191. Springer, Heidelberg (2011)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Libal, T., Riener, M., Rukhaia, M.: Advanced Proof Viewing in ProofTool. In: Benzm\u00fcller, C., Paleo, B.W. (eds.) Proceedings of the 11th Workshop on User Interfaces for Theorem Provers (UITP) 2014, EPTCS, vol. 167, pp. 35\u201347 (2014)","DOI":"10.4204\/EPTCS.167.6"},{"issue":"4","key":"20_CR15","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D Miller","year":"1987","unstructured":"Miller, D.: A compact representation of proofs. Stud. Logica 46(4), 347\u2013370 (1987)","journal-title":"Stud. Logica"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Miller, D.: ProofCert: broad spectrum proof certificates. An ERC Advanced Grant funded for the five years 2012\u20132016. \n                      http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/ProofCert.pdf","DOI":"10.21820\/23987073.2017.3.68"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Reis, G.: Importing SMT and connection proofs as expansion trees. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), EPTCS, vol. 186, pp. 3\u201310 (2015)","DOI":"10.4204\/EPTCS.186.3"},{"key":"20_CR18","unstructured":"Stasko, J., Zhang, E.: Focus+context display and navigation techniques for enhancing radial, space-filling hierarchy visualizations. In: IEEE Symposium on Information Visualization, 2000, InfoVis 2000, pp. 57\u201365 (2000)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17511-4_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP world \u2013 infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 1\u201312. Springer, Heidelberg (2010)"},{"issue":"1","key":"20_CR20","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11814771_7","volume-title":"Automated Reasoning","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 67\u201381. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T00:58:43Z","timestamp":1558313923000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"12 June 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}