{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:06Z","timestamp":1725489066941},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730835"},{"type":"electronic","value":"9783540730866"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73086-6_14","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T10:57:56Z","timestamp":1187089076000},"page":"146-160","source":"Crossref","is-referenced-by-count":5,"title":["Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User Interaction with the Matita Proof Assistant. Journal of Automated Reasoning, Special Issue on User. Interfaces for Theorem Proving (to appear)"},{"key":"14_CR2","unstructured":"Ayache, N., Filli\u00e2tre, J.C.: Combining the Coq proof assistant with first-order decision procedures (Unpublished)"},{"key":"14_CR3","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. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"14_CR4","unstructured":"D\u00e9harbe, D., Ranise, S., Fontaine, P.: haRVey, a cocktail of theories, \n                    \n                      http:\/\/harvey.loria.fr\/"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Proceedings of Theorem Proving in Higher Order Logics (TPHOL), pp. 311\u2013321 (1999)","DOI":"10.1007\/3-540-48256-3_21"},{"issue":"1-2","key":"14_CR6","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1006\/inco.2000.2913","volume":"162","author":"C. Kreitz","year":"2000","unstructured":"Kreitz, C., Schmitt, S.: A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems. Information and Computation\u00a0162(1-2), 226\u2013254 (2000)","journal-title":"Information and Computation"},{"issue":"3","key":"14_CR7","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. Mc Cune","year":"1997","unstructured":"Mc Cune, W.: Solution of the Robbins Problem. Journal of Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR8","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","author":"J. Meng","year":"2004","unstructured":"Meng, J., Paulson, L.: Experiments On Supporting Interactive Proof Using Resolution. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, Springer, Heidelberg (2004)"},{"key":"14_CR9","unstructured":"Meng, J., Paulson, L.: Translating Higher-Order Problems to First-Order Clauses. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR: Empirically Successful Computerized Reasoning. CEUR Workshop Proceedings, vol.\u00a0192, pp. 70\u201380 (2006)"},{"issue":"10","key":"14_CR10","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.: Automation for Interactive Proof: First Prototype. Information and Computation\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Information and Computation"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. Handbook of Automated Reasoning, 371\u2013443 (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"14_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/11814771_27","volume-title":"Automated Reasoning","author":"S. Obua","year":"2006","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 298\u2013302. Springer, Heidelberg (2006)"},{"key":"14_CR13","unstructured":"Paulin-Mohring, C.: D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u0155ieur. Habilitation \u00e0 diriger les recherches, Universit\u00e9 Claude Bernard Lyon I (1996)"},{"issue":"2-3","key":"14_CR14","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"},{"key":"14_CR15","unstructured":"Riazanov, A.: Implementing an Efficient Theorem Prover. PHD thesis, The University of Manchester (2003)"},{"key":"14_CR16","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)"},{"key":"14_CR17","unstructured":"Slaney, J., Fujita, M., Stickel, M.: Automated Reasoning and Exhaustive Search: Quasigroup Existence Problems. Computers and Mathematics with Applications (1993)"},{"issue":"2","key":"14_CR18","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"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"T. Tammet","year":"1996","unstructured":"Tammet, T.: A resolution theorem prover for intuitionistic logic. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - Cade-13. LNCS, vol.\u00a01104, Springer, Heidelberg (1996)"},{"key":"14_CR20","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual (2006), \n                    \n                      http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"14_CR21","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. PHD thesis, Universit\u00e9 Paris VII (1994)"}],"container-title":["Lecture Notes in Computer Science","Towards Mechanized Mathematical Assistants"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73086-6_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:42Z","timestamp":1619517582000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}