乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:47:18Z","timestamp":1725472038739},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540482819"},{"type":"electronic","value":"9783540482826"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11916277_12","type":"book-chapter","created":{"date-parts":[[2006,10,17]],"date-time":"2006-10-17T14:32:59Z","timestamp":1161095579000},"page":"167-181","source":"Crossref","is-referenced-by-count":6,"title":["A Semantic Completeness Proof for TaMeD"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bonichon","sequence":"first","affiliation":[]},{"given":"Olivier","family":"Hermant","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022559","volume-title":"Computational Logic and Proof Theory","author":"B. Beckert","year":"1993","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.: The even more liberalized \u03b4-rule in free variable Semantic Tableaux. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713. Springer, Heidelberg (1993)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-540-25984-8_33","volume-title":"Automated Reasoning","author":"R. Bonichon","year":"2004","unstructured":"Bonichon, R.: TaMeD: A tableau method for deduction modulo. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol.\u00a03097, pp. 445\u2013459. Springer, Heidelberg (2004)"},{"key":"12_CR3","unstructured":"Bonichon, R., Hermant, O.: On constructive cut admissibility in deduction modulo (submitted), http:\/\/www-spi.lip6.fr\/~bonichon\/papers\/occad-fl.ps"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Cantone, D., Nicolosi Asmundo, M.: A sound framework for delta-rule variants in free variable semantic tableaux. In: FTP (2005)","DOI":"10.1007\/s10817-006-9045-y"},{"issue":"1-2","key":"12_CR5","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","volume":"166","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Voronkov, A.: The undecidability of simultaneous rigid e-unification. Theoretical Computer Science\u00a0166(1-2), 291\u2013300 (1996)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A. Degtyarev","year":"1998","unstructured":"Degtyarev, A., Voronkov, A.: What you always wanted to know about rigid e-unification. J. Autom. Reason.\u00a020(1-2), 47\u201380 (1998)","journal-title":"J. Autom. Reason."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality Reasoning in Sequent-based Calculi, ch. 10. Elsevier Science Publishers B.V, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"12_CR8","first-page":"66","volume-title":"Proceedings of the ESSLLI-2000 Student Session","author":"E. Deplagne","year":"2000","unstructured":"Deplagne, E.: Sequent calculus viewed modulo. In: Pili\u00e8re, C. (ed.) Proceedings of the ESSLLI-2000 Student Session, Birmingham, England, August 2000, pp. 66\u201376. University of Birmingham, Birmingham (2000)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a0(31), 33\u201372 (2003)","DOI":"10.1023\/A:1027357912519"},{"issue":"4","key":"12_CR10","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"The Journal of Symbolic Logic"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Term rewriting and applications","author":"G. Dowek","year":"2005","unstructured":"Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesel, J. (ed.) Term rewriting and applications. LNCS. Springer, Heidelberg (2005)"},{"key":"12_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1996","unstructured":"Fitting, M.: First Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-45744-5_46","volume-title":"Automated Reasoning","author":"M. Giese","year":"2001","unstructured":"Giese, M.: Incremental Closure of Free Variable Tableaux. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol.\u00a02083, pp. 545\u2013560. Springer, Heidelberg (2001)"},{"issue":"2","key":"12_CR14","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00881956","volume":"13","author":"R. H\u00e4hnle","year":"1994","unstructured":"H\u00e4hnle, R., Schmitt, P.: The liberalized \u03b4-rule in free variable semantic tableaux. Journal of Automated Reasoning\u00a013(2), 211\u2013221 (1994)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR15","unstructured":"Hermant, O.: M\u00e9thodes S\u00e9mantiques en D\u00e9duction Modulo. PhD thesis, Universit\u00e9 Paris 7 - Denis Diderot (2005)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Typed Lambda-Calculi and Applications, pp. 221\u2013233 (2005)","DOI":"10.1007\/11417170_17"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"405","DOI":"10.2307\/421172","volume":"2","author":"J.-L. Krivine","year":"1996","unstructured":"Krivine, J.-L.: Une preuve formelle et intuitionniste du th\u00e9or\u00e8me de compl\u00e9tude de la logique classique. The Bulletin of Symbolic Logic\u00a02, 405\u2013421 (1996)","journal-title":"The Bulletin of Symbolic Logic"},{"key":"12_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R. Smullyan","year":"1968","unstructured":"Smullyan, R.: First Order Logic. Springer, Heidelberg (1968)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-45744-5_15","volume-title":"Automated Reasoning","author":"J. Stuber","year":"2001","unstructured":"Stuber, J.: A Model-Based Completeness Proof of Extended Narrowing and Resolution. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol.\u00a02083, p. 195. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11916277_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,9]],"date-time":"2023-05-09T07:45:31Z","timestamp":1683618331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11916277_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540482819","9783540482826"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11916277_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}