{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,26]],"date-time":"2025-12-26T14:26:24Z","timestamp":1766759184129},"reference-count":186,"publisher":"Elsevier","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1016\/b978-0-444-51624-4.50005-8","type":"book-chapter","created":{"date-parts":[[2014,12,9]],"date-time":"2014-12-09T19:01:20Z","timestamp":1418151680000},"page":"215-254","source":"Crossref","is-referenced-by-count":25,"title":["Automation of Higher-Order Logic"],"prefix":"10.1016","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0010","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"J. of Logic and Computation"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0015","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","article-title":"Tps: A hybrid automatic-interactive system for developing proofs","volume":"4","author":"Andrews","year":"2006","journal-title":"J. Applied Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0020","article-title":"Theorem proving in type theory","author":"Andrews","year":"1977"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0025","series-title":"Studies in Logic and the Foundations of Mathematics","article-title":"A Transfinite Type Theory with Type Variables","author":"Andrews","year":"1965"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0030","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","article-title":"Resolution in type theory","volume":"36","author":"Andrews","year":"1971","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0035","doi-asserted-by":"crossref","first-page":"395","DOI":"10.2307\/2272982","article-title":"General models and extensionality","volume":"37","author":"Andrews","year":"1972","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0040","doi-asserted-by":"crossref","first-page":"385","DOI":"10.2307\/2272981","article-title":"General models, descriptions, and choice in type theory","volume":"37","author":"Andrews","year":"1972","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0045","series-title":"Letter to Roger Hindley dated January 22, 1973","author":"Andrews","year":"1973"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0050","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1002\/malq.19740202506","article-title":"Provability in elementary type theory","volume":"20","author":"Andrews","year":"1974","journal-title":"Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0055","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving via general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"J. ACM"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0060","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BF00248320","article-title":"On connections and higher order logic","volume":"5","author":"Andrews","year":"1989","journal-title":"J. of Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0065","first-page":"965","article-title":"Classical type theory","volume":"volume 2","author":"Andrews","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0070","series-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"Andrews","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_rf0075","series-title":"The Stanford Encyclopedia of Philosophy","article-title":"Church\u2019s type theory","author":"Andrews","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0080","first-page":"164","article-title":"TPS: A theorem proving system for type theory","author":"Andrews","year":"2000"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0085","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/BF00252180","article-title":"TPS: A theorem proving system for classical type theory","volume":"16","author":"Andrews","year":"1996","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0090","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1090\/conm\/029\/09","article-title":"Automating higher order logics","volume":"29","author":"Andrews","year":"1984","journal-title":"Contemp. Math"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0095","author":"Arthan"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0100","series-title":"Resource-Adaptive Cognitive Processes","first-page":"389","article-title":"OMEGA: Resource-adaptive processes in an automated reasoning system","author":"Autexier","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0105","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s10817-011-9233-2","article-title":"Analytic tableaux for higher-order logic with choice","volume":"47","author":"Backes","year":"2011","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0110","doi-asserted-by":"crossref","first-page":"181","DOI":"10.2307\/421013","article-title":"The impact of the lambda calculus in logic and computer science","volume":"3","author":"Barendregt","year":"1997","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0115","series-title":"Perspectives in Logic","article-title":"Lambda Calculus with Types","author":"Barendregt","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0120","series-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0125","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/s10817-006-9036-z","article-title":"Mathematical induction in Otter-lambda","volume":"36","author":"Beeson","year":"2006","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0130","article-title":"Proof theory at work: Program development in the minlog system","volume":"volume II","author":"Benl","year":"1998"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0135","series-title":"Equality and Extensionality in Automated Higher-Order Theorem Proving","author":"Benzm\u00fcller","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0140","series-title":"Proc. of CADE-16","first-page":"399","article-title":"Extensional higher-order paramodulation and RUE-resolution","author":"Benzm\u00fcller","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0145","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1020840027781","article-title":"Comparing approaches to resolution based higher-order theorem proving","volume":"133","author":"Benzm\u00fcller","year":"2002","journal-title":"Synthese"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0150","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s10472-011-9249-7","article-title":"Combining and automating classical and non-classical logics in classical higher-order logic","volume":"62","author":"Benzm\u00fcller","year":"2011","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0155","series-title":"Proc. of IJCAI-23","article-title":"Automating quantified conditional logics in HOL","author":"Benzm\u00fcller","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0160","doi-asserted-by":"crossref","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","article-title":"Higher-order semantics and extensionality","volume":"69","author":"Benzm\u00fcller","year":"2004","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0165","series-title":"Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday","first-page":"84","article-title":"Cut elimination with xi-functionality","author":"Benzm\u00fcller","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0170","first-page":"1","article-title":"Cut-simulation and impredicativity","volume":"5","author":"Benzm\u00fcller","year":"2009","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0175","series-title":"Proceedings of CADE-14","article-title":"OMEGA: Towards a mathematical assistant","author":"Benzm\u00fcller","year":"1997"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0180","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/s10472-012-9320-z","article-title":"Embedding and automating conditional logics in classical higher-order logic","volume":"66","author":"Benzm\u00fcller","year":"2012","journal-title":"Ann. Math. Artif. Intell."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0185","series-title":"Proc. of CADE-15","first-page":"139","article-title":"LEO \u2013 a higher-order theorem prover","author":"Benzm\u00fcller","year":"1998"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_rf0190","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","article-title":"Quantified multimodal logics in simple type theory","volume":"7","author":"Benzm\u00fcller","year":"2013","journal-title":"Logica Universalis (Special Issue on Multimodal Logics)"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0195","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1016\/j.websem.2011.11.008","article-title":"Higher-order aspects and context in SUMO","volume":"12-13","author":"Benzm\u00fcller","year":"2012","journal-title":"Journal of Web Semantics"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0200","series-title":"Proceedings of LPAR-19","article-title":"HOL based first-order modal logic provers","author":"Benzm\u00fcller","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0205","series-title":"PxTP 2013","first-page":"2","article-title":"LEO-II version 1.5","author":"Benzm\u00fcller","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0210","series-title":"Proc. of IJCAR 2008","first-page":"162","article-title":"LEO-II - a cooperative automatic theorem prover for higher-order logic (system description)","author":"Benzm\u00fcller","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0215","series-title":"Formalization, Mechanization and Automation of G\u00f6del\u2019s Proof of God\u2019s Existence","author":"Benzm\u00fcller","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0220","series-title":"Texts in Theoretical Computer Science","article-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0225","series-title":"Mating Search Without Path Enumeration","author":"Bishop","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0230","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","article-title":"Extending Sledgehammer with SMT solvers","volume":"51","author":"Blanchette","year":"2013","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0235","series-title":"Proc. of TACAS-19","first-page":"493","article-title":"Encoding monomorphic and polymorphic types","author":"Blanchette","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0240","series-title":"Proc. of ITP 2010","first-page":"131","article-title":"Nitpick: A counterexample generator for higher-order logic based on a relational model finder","author":"Blanchette","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0245","first-page":"113","article-title":"Nitpicking C++ concurrency","author":"Blanchette","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0250","series-title":"Machine Intelligence 9","first-page":"53","article-title":"A maximal method for set variables in automatic theorem-proving","author":"Bledsoe","year":"1979"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0255","series-title":"PxTP 2012","first-page":"28","article-title":"The lambda-pi-calculus modulo as a universal proof language","author":"Boespflug","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0260","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00250612","article-title":"A curious inference","volume":"16","author":"Boolos","year":"1987","journal-title":"Journal of Philosophical Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0265","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","article-title":"Satallax: an automatic higher-order prover","author":"Brown","year":"2012","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0270","series-title":"Proc. of CADE-18","first-page":"408","article-title":"Solving for set variables in higher-order theorem proving","author":"Brown","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0275","series-title":"Set Comprehension in Church\u2019s Type Theory","author":"Brown","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0280","series-title":"Proc. of CADE-20","first-page":"23","article-title":"Reasoning in extensional type theory with equality","author":"Brown","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0285","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s10817-013-9283-8","article-title":"Reducing higher-order theorem proving to a sequence of sat problems","volume":"51","author":"Brown","year":"2013","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0290","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-6(2:3)2010","article-title":"Analytic tableaux for simple type theory and its first-order fragment","volume":"6","author":"Brown","year":"2010","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0295","first-page":"647","article-title":"The Oyster-Clam system","author":"Bundy","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0300","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(1:3)2011","article-title":"Efficiently simulating higher-order arithmetic by a first-order theory modulo","volume":"7","author":"Burel","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0305","series-title":"Proc. of CADE-23","first-page":"162","article-title":"Experimenting with deduction modulo","author":"Burel","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_rf0310","doi-asserted-by":"crossref","first-page":"346","DOI":"10.2307\/1968337","article-title":"A set of postulates for the foundation of logic","volume":"33","author":"Church","year":"1932","journal-title":"Annals of Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0315","doi-asserted-by":"crossref","first-page":"354","DOI":"10.2307\/2371045","article-title":"An unsolvable problem of elementary number theory","volume":"58","author":"Church","year":"1936","journal-title":"American Journal of Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0320","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0325","series-title":"The Limits of Science: Outline of Logic and of the Methodology of the Exact Sciences","author":"Chwistek","year":"1948"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0330","first-page":"913","article-title":"Inductionless induction","volume":"volume I","author":"Comon","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0335","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0340","series-title":"Proc. of LMF99: Workshop on Logical Frameworks and Meta-languages","article-title":"Structured type theory","author":"Coquand","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0345","first-page":"102","article-title":"Embedding pure type systems in the lambda-pi-calculus modulo","author":"Cousineau","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0350","doi-asserted-by":"crossref","first-page":"115","DOI":"10.2307\/2269292","article-title":"The inconsistency of certain formal logics","volume":"7","author":"Curry","year":"1942","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0355","first-page":"279","article-title":"IsaPlanner: A prototype proof planner in isabelle","author":"Dixon","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0360","series-title":"7th Symp. on Logic in Computer Science","first-page":"2","article-title":"Third order matching is decidable","author":"Dowek","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0365","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1093\/logcom\/3.3.287","article-title":"A complete proof synthesis method for the cube of type systems","volume":"3","author":"Dowek","year":"1993","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0370","first-page":"1009","article-title":"Higher-order unification and matching","volume":"volume II","author":"Dowek","year":"2001"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0375","series-title":"Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday","first-page":"244","article-title":"Skolemization in simple type theory: the logical and the theoretical points of view","author":"Dowek","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0380","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129500003236","article-title":"HOL-\u03bb\u03c3 an intentional first-order expression of higher-order logic","volume":"11","author":"Dowek","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0385","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1023\/A:1027357912519","article-title":"Theorem proving modulo","volume":"31","author":"Dowek","year":"2003","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0390","series-title":"A Mathematical Introduction to Logic","author":"Enderton","year":"1972"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0395","series-title":"The Stanford Encyclopedia of Philosophy","article-title":"Second-order and higher-order logic","author":"Enderton","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0400","doi-asserted-by":"crossref","first-page":"1269","DOI":"10.2307\/2274487","article-title":"A partial functions version of church\u2019s simple theory of types","volume":"55","author":"Farmer","year":"1990","journal-title":"J. Symb. Log."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0405","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","article-title":"IMPS: An interactive mathematical proof system","volume":"11","author":"Farmer","year":"1993","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0410","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/j.jal.2007.11.001","article-title":"The seven virtues of simple type theory","volume":"6","author":"Farmer","year":"2008","journal-title":"J. Applied Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0415","first-page":"567","article-title":"Little theories","author":"Farmer","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0420","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(99)00175-9","article-title":"The calculus of constructions as a framework for proof search with set variable instantiation","volume":"232","author":"Felty","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0425","series-title":"Begriffsschrift, eine der arithmetischen nachgebildete Formel-sprache des reinen Denkens","author":"Frege","year":"1879"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_rf0430","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/s10817-011-9218-1","article-title":"A two-level logic approach to reasoning about computations","volume":"49","author":"Gacek","year":"2012","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0435","series-title":"The Collected Papers of Gerhard Gentzen","first-page":"68","article-title":"Investigations into logical deduction","author":"Gentzen","year":"1969"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0440","series-title":"Collected Papers of Gerhard Gentzen","first-page":"252","article-title":"New version of the consistency proof for elementary number theory","author":"Gentzen","year":"1969"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0445","first-page":"63","article-title":"Une extension de l\u2019interpretation de G\u00f6del \u00e0 l\u2019analyse, et son application \u00e0 l\u2019elimination des coupures dans l\u2019analyse et la th\u00e9orie des types","author":"Girard","year":"1971"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0450","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","article-title":"The system F of variable types: Fifteen years later","volume":"45","author":"Girard","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0455","series-title":"\u00dcber die Vollst\u00e4ndigkeit des Logikkalk\u00fcls","author":"G\u00f6del","year":"1929"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0460","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF01696781","article-title":"Die vollst\u00e4ndigkeit der axiome des logischen funktionenkalk\u00fcls","volume":"37","author":"G\u00f6del","year":"1930","journal-title":"Monatshefte f\u00fcr Mathematik"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0465","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF01696781","article-title":"Die Vollst\u00e4ndigkeit der Axiome des logischen Funktionenkalk\u00fcls","volume":"37","author":"G\u00f6del","year":"1930","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0470","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","article-title":"\u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I","volume":"38","author":"G\u00f6del","year":"1931","journal-title":"Monatshefte der Mathematischen Physik"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0475","series-title":"Ergebnisse eines Mathematischen Kolloquiums","first-page":"23","article-title":"\u00dcber die L\u00e4nge von Beweisen","author":"G\u00f6del","year":"1936"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0480","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0485","series-title":"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic","author":"Gordon","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0490","series-title":"Edinburgh LCF. volume 78 of LNCS","author":"Gordon","year":"1979"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0495","series-title":"A Matching Procedure for \u03c9-Order Logic","author":"Gould","year":"1966"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0500","series-title":"Scientific Report No 1. A F C R L","first-page":"64","article-title":"Automated logic for semi-automated mathematics","author":"Guard","year":"1964"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0505","series-title":"Proc. of ICFEM 2011","first-page":"617","article-title":"Automating algebraic methods in isabelle","author":"Guttmann","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0510","series-title":"Mathematics in the Age of the Turing Machine","author":"Hales","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0515","first-page":"60","article-title":"HOL Light: An overview","author":"Harrison","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0520","series-title":"Source books in the history of the sciences series","article-title":"From Frege to G\u00f6del: A Source Book in Mathematics, 1879-1931","author":"van Heijenoort","year":"1967"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0525","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"15","author":"Henkin","year":"1950","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0530","doi-asserted-by":"crossref","first-page":"323","DOI":"10.4064\/fm-52-3-323-344","article-title":"A theory of propositional types","author":"Henkin","year":"1963","journal-title":"Fundamatae Mathematicae"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0535","first-page":"71","article-title":"N-sorted logic for automatic theorem-proving in higher-order logic","author":"Henschen","year":"1972"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0540","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1093\/logcom\/exp076","article-title":"Completeness and cut-elimination in the intuitionistic theory of types - part 2","volume":"20","author":"Hermant","year":"2010","journal-title":"J. Logic and Computation"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0545","series-title":"Festschrift zur Feier der Enthllung des Gauss-Weber-Denkmals in G\u00f6ttingen","first-page":"1","article-title":"Grundlagen der geometrie","author":"Hilbert","year":"1899"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0550","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1023\/A:1010652212067","article-title":"The Watson theorem prover","volume":"26","author":"Holmes","year":"2001","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_rf0555","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","article-title":"The undecidability of unification in third order logic","volume":"22","author":"Huet","year":"1973","journal-title":"Information and Control"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0560","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0565","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","article-title":"Proving and applying program transformations expressed with second-order patterns","volume":"11","author":"Huet","year":"1978","journal-title":"Acta Informatica"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0570","series-title":"Constrained Resolution: A Complete Method for Higher Order Logic","author":"Huet","year":"1972"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0575","first-page":"139","article-title":"A mechanization of type theory","author":"Huet","year":"1973"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0580","series-title":"Design and Application of Strategies\/Tactics in Higher Order Logics","first-page":"56","article-title":"First-order proof tactics in higher-order logic theorem provers","author":"Hurd","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0585","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","article-title":"Mechanizing omega-order type theory through unification","volume":"3","author":"Jensen","year":"1976","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0590","series-title":"Learning-assisted automated reasoning with flyspeck","author":"Kaliszyk","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0595","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1109\/32.588534","article-title":"An industrial strength theorem prover for a logic based on Common Lisp","volume":"23","author":"Kaufmann","year":"1997","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0600","series-title":"Proc. of IJCAI-12","first-page":"137","article-title":"How to prove higher order theorems in first order logic","author":"Kerber","year":"1991"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0605","series-title":"Proc. of ECAI","first-page":"145","article-title":"On the translation of higher-order problems into first-order logic","author":"Kerber","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0610","doi-asserted-by":"crossref","first-page":"630","DOI":"10.2307\/1968646","article-title":"The inconsistency of certain formal logics","volume":"36","author":"Kleene","year":"1935","journal-title":"Annals of Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0615","series-title":"A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle","author":"Kohlhase","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0620","first-page":"229","article-title":"Higher-order logic","volume":"volume 2","author":"Leivant","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0625","doi-asserted-by":"crossref","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","article-title":"Focusing and polarization in linear, intuitionistic, and classical logics","volume":"410","author":"Liang","year":"2009","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0630","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10817-004-6885-1","article-title":"Choices in representing and reduction strategies for lambda terms in intensional contexts","volume":"33","author":"Liang","year":"2005","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0635","series-title":"agsyHOL website","author":"Lindblad","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0640","series-title":"Technical Report Report CSRR 2059","article-title":"The Undecidability of Unification for Third Order Languages","author":"Lucchesi","year":"1972"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0645","series-title":"Sixth International Congress for Logic, Methodology, and Philosophy of Science","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f","year":"1982"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0650","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1145\/504077.504080","article-title":"Reasoning with higher-order abstract syntax in a logical framework","volume":"3","author":"McDowell","year":"2002","journal-title":"ACM Trans. Comput. Log."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0655","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","article-title":"Translating higher-order clauses to first-order clauses","volume":"40","author":"Meng","year":"2008","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0660","series-title":"Proofs in Higher-Order Logic","author":"Miller","year":"1983"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0665","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/BF00370646","article-title":"A compact representation of proofs","volume":"46","author":"Miller","year":"1987","journal-title":"Studia Logica"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0670","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","article-title":"A logic programming language with lambda-abstraction, function variables, and simple unification","volume":"4","author":"Miller","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0675","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","article-title":"Unification under a mixed prefix","volume":"14","author":"Miller","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0680","first-page":"54","article-title":"A proposal for broad spectrum proof certificates","author":"Miller","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0685","series-title":"Programming with Higher-Order Logic","author":"Miller","year":"2012"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_rf0690","first-page":"50","article-title":"A look at TPS","author":"Miller","year":"1982"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0695","doi-asserted-by":"crossref","first-page":"479","DOI":"10.2307\/2586480","article-title":"Cut-elimination for simple type theory with an axiom of choice","volume":"64","author":"Mints","year":"1999","journal-title":"J. Symb. Log."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0700","series-title":"Proceedings of TACAS 2007","first-page":"519","article-title":"The heterogeneous tool set, Hets","author":"Mossakowski","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0705","doi-asserted-by":"crossref","first-page":"98","DOI":"10.2178\/jsl\/1174668386","article-title":"Intensional models for the theory of types","volume":"72","author":"Muskens","year":"2007","journal-title":"J. Symb. Log."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0710","first-page":"371","article-title":"Practical higher-order pattern unification with on-the-fly raising","author":"Nadathur","year":"2005"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0715","first-page":"810","article-title":"An Overview of \u03bbProlog","author":"Nadathur","year":"1988"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0720","series-title":"Selected Papers on Automath","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0725","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0167-6423(89)90038-5","article-title":"Equational reasoning in Isabelle","volume":"12","author":"Nipkow","year":"1989","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0730","series-title":"Number 2283 in LNCS","article-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0735","first-page":"748","article-title":"PVS: A Prototype Verification System","author":"Owre","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0740","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1017\/S0960129500003108","article-title":"Decidability of fourth-order matching","volume":"10","author":"Padovani","year":"2000","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0745","first-page":"29","article-title":"Some results on the length of proofs","volume":"177","author":"Parikh","year":"1973","journal-title":"Transactions of the ACM"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0750","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","article-title":"The foundation of a generic theorem prover","volume":"5","author":"Paulson","year":"1989","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0755","series-title":"Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)","author":"Paulson","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0760","first-page":"51","article-title":"A generic tableau prover and its integration with isabelle","volume":"5","author":"Paulson","year":"1999","journal-title":"Journal of Universal Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0765","series-title":"Arithmetices principia, nova methodo exposita","author":"Peano","year":"1889"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0770","series-title":"Proof Transformations in Higher-Order Logic","first-page":"156","author":"Pfenning","year":"1987"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0775","first-page":"811","article-title":"Elf: A meta-language for deductive systems (system descrition)","author":"Pfenning","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0780","first-page":"202","article-title":"System description: Twelf - a meta-logical framework for deductive systems","author":"Pfenning","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0785","first-page":"15","article-title":"Beluga: A framework for programming and reasoning with deductive systems (system description)","author":"Pientka","year":"2010"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0790","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/321752.321764","article-title":"A complete mechanization of second-order type theory","volume":"20","author":"Pietrzykowski","year":"1973","journal-title":"J. ACM"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0795","first-page":"82","article-title":"A complete mechanization of \u03c9-order type theory","author":"Pietrzykowski","year":"1972"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0800","series-title":"The Theory of LEGO","author":"Pollack","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0805","doi-asserted-by":"crossref","first-page":"452","DOI":"10.2307\/2270331","article-title":"Hauptsatz for higher order logic","volume":"33","author":"Prawitz","year":"1968","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0810","series-title":"Mathematical Logic","author":"Quine","year":"1940"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_rf0815","series-title":"Proceedings of the London Mathematical Society","first-page":"338","article-title":"The foundations of mathematics","author":"Ramsey","year":"1926"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0820","series-title":"Colloque sur la Programmation","first-page":"408","article-title":"Towards a theory of type structure","author":"Reynolds","year":"1974"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0825","first-page":"129","article-title":"System description: Proof planning in higher-order logic with lambda-Clam","author":"Richardson","year":"1998"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0830","series-title":"Machine Intelligence 4","first-page":"151","article-title":"Mechanizing higher-order logic","author":"Robinson","year":"1969"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0835","series-title":"Machine Intelligence 5","first-page":"121","article-title":"A note on mechanizing higher order logic","author":"Robinson","year":"1970"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0840","series-title":"Letter to Frege","author":"Russell","year":"1902"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0845","series-title":"The principles of mathematics","author":"Russell","year":"1903"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0850","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","article-title":"Mathematical logic as based on the theory of types","volume":"30","author":"Russell","year":"1908","journal-title":"American Journal of Mathematics"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0855","first-page":"111","article-title":"E \u2013 a brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Communications"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0860","doi-asserted-by":"crossref","first-page":"305","DOI":"10.2307\/2963525","article-title":"Semantical and syntactical properties of simple type theory","volume":"25","author":"Sch\u00fctte","year":"1960","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0865","doi-asserted-by":"crossref","first-page":"714","DOI":"10.2307\/2274326","article-title":"Second-order languages and mathematical practice","volume":"50","author":"Shapiro","year":"1985","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0870","doi-asserted-by":"crossref","first-page":"828","DOI":"10.1073\/pnas.49.6.828","article-title":"A unifying principle for quantification theory","volume":"49","author":"Smullyan","year":"1963","journal-title":"Proc. Nat. Acad Sciences"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0875","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","article-title":"Higher order unification revisited: Complete sets of transformations","volume":"8","author":"Snyder","year":"1989","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0880","series-title":"FOSSACS\u201903","first-page":"425","article-title":"On the structure of inductive reasoning: Circular and tree-shaped proofs in the \u03bc-calculus","author":"Spenger","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0885","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-5(3:2)2009","article-title":"Decidability of higher-order matching","volume":"5","author":"Stirling","year":"2009","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0890","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","article-title":"The TPTP problem library and associated infrastructure","volume":"43","author":"Sutcliffe","year":"2009","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0895","first-page":"1","article-title":"Automated reasoning in higher-order logic using the TPTP THF infrastructure","volume":"3","author":"Sutcliffe","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0900","doi-asserted-by":"crossref","first-page":"980","DOI":"10.1090\/S0002-9904-1966-11611-7","article-title":"A nonconstructive proof of Gentzen\u2019s Hauptsatz for second order predicate logic","volume":"72","author":"Tait","year":"1966","journal-title":"Bulletin of the American Mathematical Society"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0905","doi-asserted-by":"crossref","first-page":"399","DOI":"10.2969\/jmsj\/01940399","article-title":"A proof of cut-elimination theorem in simple type theory","volume":"19","author":"Takahashi","year":"1967","journal-title":"Journal of the Mathematical Society of Japan"},{"issue":"1954","key":"10.1016\/B978-0-444-51624-4.50005-8_bb0910","first-page":"149","article-title":"On a generalized logic calculus","volume":"24","author":"Takeuti","year":"1953","journal-title":"Japanese Journal of Mathematics 23, 39-96. Errata: ibid, vol."},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0915","doi-asserted-by":"crossref","first-page":"238","DOI":"10.2969\/jmsj\/01230238","article-title":"An example on the fundamental conjecture of GLC","volume":"12","author":"Takeuti","year":"1960","journal-title":"Journal of the Mathematical Society of Japan"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0920","series-title":"Proof Theory. volume 81 of Studies in Logic and the Foundations of Mathematics","author":"Takeuti","year":"1975"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0925","series-title":"The Stanford Encyclopedia of Philosophy","article-title":"Generalized quantifiers","author":"Westerst\u00e5hl","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0930","series-title":"Principia Mathematica","author":"Whitehead","year":"1910"},{"key":"10.1016\/B978-0-444-51624-4.50005-8_bb0935","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","article-title":"Descente infinie + deduction","volume":"12","author":"Wirth","year":"2004","journal-title":"Logic Journal of the IGPL"}],"container-title":["Handbook of the History of Logic","Computational Logic"],"original-title":[],"link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444516244500058?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444516244500058?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T08:41:29Z","timestamp":1566117689000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444516244500058"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":186,"URL":"https:\/\/doi.org\/10.1016\/b978-0-444-51624-4.50005-8","relation":{},"ISSN":["1874-5857"],"issn-type":[{"value":"1874-5857","type":"print"}],"subject":[],"published":{"date-parts":[[2014]]}}}