{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:16:45Z","timestamp":1725560205437},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_2","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"7-22","source":"Crossref","is-referenced-by-count":5,"title":["Reflecting Proofs in First-Order Logic with Equality"],"prefix":"10.1007","author":[{"given":"Evelyne","family":"Contejean","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Corbineau","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Alvarado, C.: R\u00e9flexion pour la r\u00e9\u00e9criture dans le calcul des constructions inductives. PhD thesis, Universit\u00e9 Paris-Sud (December 2002)"},{"key":"2_CR2","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, ch. 1","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, ch. 1, pp. 1\u201330. Academic Press, New York (1989)"},{"issue":"3","key":"2_CR3","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. Journal of Automated Reasoning\u00a029(3), 253\u2013275 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR4","unstructured":"Contejean, E., March\u00e9, C., Urbain, X.: CiME3 (2004), \n                  \n                    http:\/\/cime.lri.fr\/"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-24849-1_11","volume-title":"Types for Proofs and Programs","author":"P. Corbineau","year":"2004","unstructured":"Corbineau, P.: First-order reasoning in the calculus of inductive constructions. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 162\u2013177. Springer, Heidelberg (2004)"},{"key":"2_CR6","unstructured":"Cr\u00e9gut, P.: Une proc\u00e9dure de d\u00e9cision r\u00e9flexive pour l\u2019arithm\u00e9tique de Presburger en Coq. Deliverable, Projet RNRT Calife (2001)"},{"issue":"5","key":"2_CR7","first-page":"380","volume":"75","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Proc. of the Koninklijke Nederlands Akademie\u00a075(5), 380\u2013392 (1972)","journal-title":"Proc. of the Koninklijke Nederlands Akademie"},{"issue":"3","key":"2_CR8","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic\u00a057(3), 795\u2013807 (1992)","journal-title":"The Journal of Symbolic Logic"},{"key":"2_CR9","first-page":"235","volume-title":"International Conference on Functional Programming 2002","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming 2002, pp. 235\u2013246. ACM Press, New York (2002)"},{"key":"2_CR10","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)"},{"issue":"3-4","key":"2_CR11","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1023\/A:1021923116629","volume":"29","author":"D. Hendriks","year":"2002","unstructured":"Hendriks, D.: Proof Reflection in Coq. Journal of Automated Reasoning\u00a029(3-4), 277\u2013307 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/3-540-45620-1_38","volume-title":"Automated Deduction - CADE-18","author":"T. Hillenbrand","year":"2002","unstructured":"Hillenbrand, T., L\u00f6chner, B.: The next WALDMEISTER loop. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 486\u2013500. Springer, Heidelberg (2002)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Automata, Languages and Programming","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 54\u201371. Springer, Heidelberg (1987)"},{"key":"2_CR14","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of the International Workshop RULE 2001","author":"Q.-H. Nguyen","year":"2001","unstructured":"Nguyen, Q.-H.: Certifying Term Rewriting Proofs in ELAN. In: van den Brand, M., Verma, R. (eds.) Proceedings of the International Workshop RULE 2001. Electronic Notes in Theoretical Computer Science, vol.\u00a059, Elsevier Science Publishers, Amsterdam (2001)"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G.E. Peterson","year":"1983","unstructured":"Peterson, G.E.: A technique for establishing completeness results in theorem proving with equality. SIAM Journal on Computing\u00a012(1), 82\u2013100 (1983)","journal-title":"SIAM Journal on Computing"},{"issue":"2","key":"2_CR16","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR17","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual \u2013 Version V8.0 (April 2004), \n                  \n                    http:\/\/coq.inria.fr"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:09:09Z","timestamp":1605643749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11532231_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}