{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:00:58Z","timestamp":1725490858943},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_18","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"263-278","source":"Crossref","is-referenced-by-count":10,"title":["Handling Polymorphism in Automated Deduction"],"prefix":"10.1007","author":[{"given":"Jean-Fran\u00e7ois","family":"Couchot","sequence":"first","affiliation":[]},{"given":"St\u00e9phane","family":"Lescuyer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","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.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"18_CR2","volume-title":"Coq\u2019Art: the Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. In: Coq\u2019Art: the Calculus of Inductive Constructions, Springer, Heidelberg (2004)"},{"issue":"3","key":"18_CR3","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a Theorem Prover for Program Checking. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"unstructured":"D\u00e9harbe, D., Ranise, S.: BDD-driven First-Order Satisfiability Procedures (extended version). Technical Report 4630, LORIA (2002)","key":"18_CR4"},{"unstructured":"Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2006), \n                    \n                      http:\/\/www.SMT-LIB.org","key":"18_CR5"},{"unstructured":"Dutertre, B., de Moura, L.: The YICES SMT Solver (2006), avaliable at \n                    \n                      http:\/\/yices.csl.sri.com\/tool-paper.pdf","key":"18_CR6"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"unstructured":"Couchot, J.F., Lescuyer, S.: Handling Polymorphism in Automated Deduction (2007), Available at \n                    \n                      http:\/\/lri.fr\/~couchot\/ftp\/publis\/CL07t.ps","key":"18_CR8"},{"unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Ac. Press, Inc. (1972)","key":"18_CR9"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Journal of Information and computation\u00a0183, 140\u2013164 (2003)","journal-title":"Journal of Information and computation"},{"unstructured":"Lescuyer, S.: Codage de la logique du premier ordre polymorphe multi-sort\u00e9e dans la logique sans sortes. Master\u2019s thesis (in english), pp. 28\u201358 (2006)","key":"18_CR11"},{"issue":"8","key":"18_CR12","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The Omega Test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a035(8), 102\u2013114 (1992)","journal-title":"Communications of the ACM"},{"unstructured":"Ayache, N., Filli\u00e2tre, J.C.: Combining the Coq Proof Assistant with First-Order Decision Procedures. Unpublished (March 2006)","key":"18_CR13"},{"unstructured":"Filli\u00e2tre, J.C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (March 2003)","key":"18_CR14"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-46508-1_9","volume-title":"Selected Papers from Automated Deduction in Classical and Non-Classical Logics","author":"I. Dahn","year":"2000","unstructured":"Dahn, I.: Interpretation of a mizar-like logic in first-order logic. In: Selected Papers from Automated Deduction in Classical and Non-Classical Logics, pp. 137\u2013151. Springer, London (2000)"},{"key":"18_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-45744-5_34","volume-title":"Automated Reasoning","author":"S. Schmitt","year":"2001","unstructured":"Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: Jprover: Integrating connection-based theorem proving into interactive proof assistants. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 421\u2013426. Springer, Heidelberg (2001)"},{"unstructured":"Rudnicki, P.: An overview of the Mizar project. In: Workshop on Types for Proofs and Programs, pp. 311\u2013330 (1992)","key":"18_CR18"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/10721959_12","volume-title":"Automated Deduction - CADE-17","author":"S.F. Allen","year":"2000","unstructured":"Allen, S.F., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L.: The nuprl open logical environment. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, pp. 170\u2013176. Springer, Heidelberg (2000)"},{"unstructured":"Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. Technical Report NASA\/CP-2003-212448, NASA (2003)","key":"18_CR20"},{"unstructured":"Meng, J., Paulson, L.C.: Translating Higher-Order Problems to First-Order Clauses. In: ESCoR (CEUR Workshop Proceedings), vol. 192, pp. 70\u201380 (2006)","key":"18_CR21"},{"issue":"10","key":"18_CR22","doi-asserted-by":"publisher","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: first prototype. Inf. Comput.\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Inf. Comput."},{"key":"18_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System Description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"18_CR24","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and Implementation of VAMPIRE. AI Commun.\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"3","key":"18_CR25","first-page":"73","volume":"5","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. J. UCS: Journal of Universal Computer Science\u00a05(3), 73 (1999)","journal-title":"J. UCS: Journal of Universal Computer Science"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-69738-1_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C. Bouillaguet","year":"2007","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 74\u201388. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:02Z","timestamp":1619502782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}