{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:36:26Z","timestamp":1725550586492},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540290513"},{"type":"electronic","value":"9783540317302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11559306_17","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T12:50:36Z","timestamp":1127825436000},"page":"285-301","source":"Crossref","is-referenced-by-count":10,"title":["Connecting a Logical Framework to a First-Order Logic Prover"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"given":"Ulf","family":"Norell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/11417170_4","volume-title":"Typed Lambda Calculi and Applications","author":"A. Abel","year":"2005","unstructured":"Abel, A., Coquand, T.: Untyped algorithmic equality for Martin-L\u00f6f\u2019s logical framework with surjective pairs. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 23\u201338. Springer, Heidelberg (2005)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A., Coquand, T., Norell, U.: Connecting a logical framework to a first-order logic prover (extended version). Technical report, Department of Computing Science, Chalmers University of Technology, Gothenburg, Sweden (2005), Available under http:\/\/www.cs.chalmers.se\/~ulfn\/papers\/fol.html","DOI":"10.1007\/11559306_17"},{"key":"17_CR3","unstructured":"Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter (April 2005) (Manuscript, available online)"},{"key":"17_CR4","unstructured":"Beeson, M.: Otter-\u03bb home page (2005), http:\/\/mh215a.cs.sjsu.edu\/"},{"key":"17_CR5","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","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. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"17_CR6","first-page":"86","volume":"79","author":"M. Bezem","year":"2003","unstructured":"Bezem, M., Coquand, T.: Newman\u2019s lemma \u2013 a case study in proof automation and geometric logic. Bulletin of the EATCS\u00a079, 86\u2013100 (2003); Logic in Computer Science Column","journal-title":"Bulletin of the EATCS"},{"issue":"3\u20134","key":"17_CR7","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. JAR\u00a029(3\u20134), 253\u2013275 (2002); Special Issue Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn","journal-title":"JAR"},{"issue":"9","key":"17_CR8","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/357766.351266","volume":"35","author":"K. Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices\u00a035(9), 268\u2013279 (2000)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR9","unstructured":"Coquand, C., Coquand, T.: Structured type theory. In: Workshop on Logical Frameworks and Meta-languages (LFM 1999), Paris, France (September 1999)"},{"issue":"3","key":"17_CR10","first-page":"203","volume":"111","author":"M. Coste","year":"2001","unstructured":"Coste, M., Lombardi, H., Roy, M.-F.: Dynamical methods in algebra: Effective Nullstellens\u00e4tze. APAL\u00a0111(3), 203\u2013256 (2001)","journal-title":"APAL"},{"key":"17_CR11","first-page":"579","volume-title":"To H. B. Curry: Essays in combinatory logic, lambda calculus and formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project Automath. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays in combinatory logic, lambda calculus and formalism, pp. 579\u2013606. Academic Press, London (1980)"},{"issue":"176\u2013210","key":"17_CR12","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift\u00a039(176\u2013210), 405\u2013431 (1935)","journal-title":"Mathematische Zeitschrift"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"788","DOI":"10.1007\/3-540-58156-1_61","volume-title":"CADE 1994","author":"X. Huang","year":"1994","unstructured":"Huang, X., Kerber, M., Kohlhase, M., Melis, E., Nesmith, D., Richts, J., Siekmann, J.H.: Omega-MKRP: A proof development environment. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 788\u2013792. Springer, Heidelberg (1994)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"key":"17_CR15","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-45620-1_10","volume-title":"Automated Deduction - CADE-18","author":"J. Hurd","year":"2002","unstructured":"Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 134\u2013138. Springer, Heidelberg (2002)"},{"key":"17_CR16","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) STRATA 2003, number CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (September 2003)"},{"key":"17_CR17","first-page":"311","volume-title":"Global Analysis in Modern Mathematics","author":"L. Lamport.","year":"1993","unstructured":"Lamport., L.: How to write a proof. In: Global Analysis in Modern Mathematics, February 1993, pp. 311\u2013321. Publish or Perish, Houston (1993); Also appeared as SRC Research Report 94"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-25984-8_28","volume-title":"Automated Reasoning","author":"J. Meng","year":"2004","unstructured":"Meng, J., Paulson, L.C.: Experiments on supporting interactive proof using resolution. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol.\u00a03097, pp. 372\u2013384. Springer, Heidelberg (2004)"},{"issue":"4","key":"17_CR19","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix. J. Symb. Comput.\u00a014(4), 321\u2013358 (1992)","journal-title":"J. Symb. Comput."},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Martin-L\u00f6f\u2019s type theory. In: Handbook of Logic in Computer Science, vol.\u00a05, OUP (October 2000)","DOI":"10.1093\/oso\/9780198537816.003.0004"},{"key":"17_CR21","volume-title":"Programming in Martin L\u00f6f\u2019s Type Theory: An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin L\u00f6f\u2019s Type Theory: An Introduction. Clarendon Press, Oxford (1990)"},{"issue":"1","key":"17_CR22","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. JACM\u00a012(1), 23\u201341 (1965)","journal-title":"JACM"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","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, vol.\u00a02083, pp. 421\u2013426. Springer, Heidelberg (2001)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0020597","volume-title":"Types for Proofs and Programs","author":"J.M. Smith","year":"1996","unstructured":"Smith, J.M., Tammet, T.: Optimized encodings of fragments of type theory in first-order logic. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 265\u2013287. Springer, Heidelberg (1996)"},{"issue":"2","key":"17_CR25","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. JAR\u00a018(2), 199\u2013204 (1997)","journal-title":"JAR"},{"issue":"2","key":"17_CR26","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF00243005","volume":"5","author":"C.A. Wick","year":"1989","unstructured":"Wick, C.A., McCune, W.: Automated reasoning about elementary point-set topology. JAR\u00a05(2), 239\u2013255 (1989)","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11559306_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T03:05:25Z","timestamp":1626577525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11559306_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540290513","9783540317302"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11559306_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}