{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:37Z","timestamp":1749124057289},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540536864"},{"type":"electronic","value":"9783540469827"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/bfb0018458","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T05:30:30Z","timestamp":1132637430000},"page":"444-453","source":"Crossref","is-referenced-by-count":5,"title":["Towards a connection procedure with built in theories"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Petermann","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"29_CR1","unstructured":"Auffray I., Enjalbert P., Modal theorem proving using equational methods, Rep. 88\u201311, Lab. d'Informatique, Univ. de Caen, 1988."},{"volume-title":"Deduction systems","year":"1987","key":"29_CR2","unstructured":"K.H. Blaesius, H.J. Bueckert (Eds.), Deduction systems (in german), Oldenbourg-Verlag, Muenchen, Wien, 1987."},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Bibel W., Computationally improved versions of Herbrand's theorem, J. Stern Ed., Proc. of Herbrand Symp., North Holland Publ. Comp., 1982.","DOI":"10.1016\/S0049-237X(08)71874-3"},{"key":"29_CR4","unstructured":"\u2014, Automated theorem proving, Verlag Vieweg, 1982, 1987."},{"key":"29_CR5","unstructured":"Herbrand J., Recherches sur la th\u00e9orie de la d\u00e9monstration, Travaux Soc. Sci. et Lettres Varsovie, Cl. 3 (Math. Phys.) (1930), 128pp, English transl. in Goldfarb W.D. (Ed.), Jaques Herbrand, Logical writings, Reidel, Dortrecht 1971."},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Petermann U., An extended Herbrand Theorem for First-order Theories with Equality Interpreted in Partial Algebras, in Kreczmar A., Mirkowska G., Eds. Proc. Math. Found. of Comp. Sci., LNCS 379.","DOI":"10.1007\/3-540-51486-4_88"},{"key":"29_CR7","unstructured":"\u2014, Building in Theories into a first-order proof procedure based on the connection method, Preprint, to appear."},{"issue":"4","key":"29_CR8","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"Stickel M., Automated deduction by theory resolution, J. Autom. Reasoning, 1, 4 (1985), 333\u2013356.","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logics in AI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018458","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:35:58Z","timestamp":1586572558000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018458"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540536864","9783540469827"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0018458","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}