{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:32:48Z","timestamp":1725535968362},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642029585"},{"type":"electronic","value":"9783642029592"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_8","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T05:02:22Z","timestamp":1248498142000},"page":"116-130","source":"Crossref","is-referenced-by-count":11,"title":["Progress in the Development of Automated Theorem Proving for Higher-Order Logic"],"prefix":"10.1007","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]},{"given":"Chad E.","family":"Brown","sequence":"additional","affiliation":[]},{"given":"Frank","family":"Theiss","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in Type Theory. Journal of Symbolic Logic\u00a036(3), 414\u2013432 (1971)","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"8_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem Proving via General Matings. Journal of the ACM\u00a028(2), 193\u2013214 (1981)","journal-title":"Journal of the ACM"},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"P.B. Andrews","year":"1989","unstructured":"Andrews, P.B.: On Connections and Higher-Order Logic. Journal of Automated Reasoning\u00a05(3), 257\u2013291 (1989)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"8_CR4","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"P.B. Andrews","year":"2006","unstructured":"Andrews, P.B., Brown, C.E.: TPS: A Hybrid Automatic-Interactive System for Developing Proofs. Journal of Applied Logic\u00a04(4), 367\u2013395 (2006)","journal-title":"Journal of Applied Logic"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: A Generic Tool for Proof Development. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 38\u201342. Springer, Heidelberg (2000)"},{"key":"8_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11541868_5","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Benzm\u00fcller","year":"2005","unstructured":"Benzm\u00fcller, C., Brown, C.E.: A Structured Set of Higher-Order Problems. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS (LNAI), vol.\u00a03603, pp. 66\u201381. Springer, Heidelberg (2005)"},{"issue":"4","key":"8_CR7","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C. Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C.E., Kohlhase, M.: Higher-order Semantics and Extensionality. Journal of Symbolic Logic\u00a069(4), 1027\u20131088 (2004)","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0054256","volume-title":"Automated Deduction - CADE-15","author":"C. Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO - A Higher-Order Theorem Prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 139\u2013143. Springer, Heidelberg (1998)"},{"unstructured":"Benzm\u00fcller, C., Paulson, L.: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. In: Benzm\u00fcller, C., Brown, C.E., Siekmann, J., Statman, R. (eds.) Reasoning in Simple Type Theory: Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Studies in Logic, Mathematical Logic and Foundations, vol.\u00a017. College Publications (2009)","key":"8_CR9"},{"unstructured":"Benzm\u00fcller, C., Paulson, L.: Exploring Properties of Propositional Normal Multimodal Logics and Propositional Intuitionistic Logics in Simple Type Theory. Journal of Symbolic Logic (submitted)","key":"8_CR10"},{"doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L., Theiss, F., Fietzke, A.: Progress Report on LEO-II - An Automatic Theorem Prover for Higher-Order Logic. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp. 33\u201348 (2007)","key":"8_CR11","DOI":"10.1007\/978-3-540-74591-4"},{"key":"8_CR12","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"8_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: THF0 - The Core TPTP Language for Classical Higher-Order Logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 491\u2013506. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined Reasoning by Automated Cooperation. Journal of Applied Logic\u00a06(3) (2008) (to appear)","key":"8_CR14","DOI":"10.1016\/j.jal.2007.06.003"},{"issue":"4","key":"8_CR15","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On Matrices with Connections. Journal of the ACM\u00a028(4), 633\u2013645 (1981)","journal-title":"Journal of the ACM"},{"key":"8_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-48660-7_32","volume-title":"Automated Deduction - CADE-16","author":"M. Bishop","year":"1999","unstructured":"Bishop, M.: A Breadth-First Strategy for Mating Search. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 359\u2013373. Springer, Heidelberg (1999)"},{"unstructured":"Brown, C.E.: Dependently Typed Set Theory. Technical Report SWP-2006-03, Saarland University (2006)","key":"8_CR17"},{"unstructured":"Brown, C.E.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church\u2019s Type Theory. Studies in Logic: Logic and Cognitive Systems, vol.\u00a010. College Publications (2007)","key":"8_CR18"},{"unstructured":"Brown, C.E.: M-Set Models. In: Benzm\u00fcller, C., Brown, C.E., Siekmann, J., Statman, R. (eds.) Reasoning in Simple Type Theory: Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Studies in Logic, Mathematical Logic and Foundations, vol.\u00a017. College Publications (2009)","key":"8_CR19"},{"doi-asserted-by":"crossref","unstructured":"Garg, D.: Principal-Centric Reasoning in Constructive Authorization Logic. Technical Report CMU-CS-09-120, School of Computer Science, Carnegie Mellon University (2009)","key":"8_CR20","DOI":"10.21236\/ADA506999"},{"issue":"1","key":"8_CR21","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A Unification Algorithm for Typed Lambda-Calculus. Theoretical Computer Science\u00a01(1), 27\u201357 (1975)","journal-title":"Theoretical Computer Science"},{"unstructured":"Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: Archer, M., Di Vito, B., Munoz, C. (eds.) Proceedings of the 1st International Workshop on Design and Application of Strategies\/Tactics in Higher Order Logics. NASA Technical Reports, number\u00a0NASA\/CP-2003-212448, pp. 56\u201368 (2003)","key":"8_CR22"},{"key":"8_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11826095","volume-title":"OMDoc - An Open Markup Format for Mathematical Documents [version 1.2]","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc - An Open Markup Format for Mathematical Documents [version 1.2]. LNCS (LNAI), vol.\u00a04180. Springer, Heidelberg (2006)"},{"unstructured":"Landau, E.: Grundlagen der Analysis. Akademische Verlagsgesellschaft M.B.H. (1930)","key":"8_CR24"},{"issue":"4","key":"8_CR25","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. Studia Logica\u00a046(4), 347\u2013370 (1987)","journal-title":"Studia Logica"},{"issue":"2-3","key":"8_CR26","first-page":"77","volume":"15","author":"R. Nieuwenhuis","year":"2002","unstructured":"Nieuwenhuis, R.: The Impact of CASC in the Development of Automated Deduction Systems. AI Communications\u00a015(2-3), 77\u201378 (2002)","journal-title":"AI Communications"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"8_CR28","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"issue":"1-2","key":"8_CR29","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T. Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP Problem Library for Intuitionistic Logic - Release v1.1. Journal of Automated Reasoning\u00a038(1-2), 261\u2013271 (2007)","journal-title":"Journal of Automated Reasoning"},{"issue":"2-3","key":"8_CR30","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"issue":"2-3","key":"8_CR31","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E: A Brainiac Theorem Prover. AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"issue":"4","key":"8_CR32","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J. Siekman","year":"2006","unstructured":"Siekman, J., Benzm\u00fcller, C., Autexier, S.: Computer Supported Mathematics with OMEGA. Journal of Applied Logic\u00a04(4), 533\u2013559 (2006)","journal-title":"Journal of Applied Logic"},{"issue":"6","key":"8_CR33","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic Derivation Verification. International Journal on Artificial Intelligence Tools\u00a015(6), 1053\u20131070 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","first-page":"7","volume-title":"Computer Science \u2013 Theory and Applications","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M., Voronkov, A. (eds.) CSR 2007. LNCS, vol.\u00a04649, pp. 7\u201323. Springer, Heidelberg (2007)"},{"unstructured":"Sutcliffe, G.: The SZS Ontologies for Automated Reasoning Software. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics. CEUR Workshop Proceedings, vol.\u00a0418, pp. 38\u201349 (2008)","key":"8_CR35"},{"key":"8_CR36","series-title":"LNAI","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.\u00a04130, pp. 67\u201381. Springer, Heidelberg (2006)"},{"issue":"1","key":"8_CR37","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"issue":"2","key":"8_CR38","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An Interactive Derivation Viewer. In: Autexier, S., Benzm\u00fcller, C. (eds.) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 3rd International Joint Conference on Automated Reasoning. Electronic Notes in Theoretical Computer Science, vol.\u00a0174, pp. 109\u2013123 (2006)","key":"8_CR39","DOI":"10.1016\/j.entcs.2006.09.025"},{"unstructured":"van Benthem Jutting, L.S.: Checking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH System. PhD thesis, Eindhoven University, Eindhoven, The Netherlands (1979)","key":"8_CR40"},{"key":"8_CR41","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814771_15","volume-title":"Automated Reasoning","author":"A. Gelder Van","year":"2006","unstructured":"Van Gelder, A., Sutcliffe, G.: Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 156\u2013161. Springer, Heidelberg (2006)"},{"key":"8_CR42","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: SPASS Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11542384","volume-title":"The Seventeen Provers of the World","author":"F. Wiedijk","year":"2006","unstructured":"Wiedijk, F.: The Seventeen Provers of the World. LNCS, vol.\u00a03600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T17:52:15Z","timestamp":1558461135000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}