{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:35Z","timestamp":1725663155684},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540502418"},{"type":"electronic","value":"9783540459606"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-50241-6_42","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:18:39Z","timestamp":1330201119000},"page":"263-272","source":"Crossref","is-referenced-by-count":0,"title":["Interfacing a logic machine"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Sch\u00f6nfeld","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"W. Bibel, Matings in Matrices, Communications of the ACM 26(1983), 844\u2013852","journal-title":"Communications of the ACM"},{"key":"18_CR2","first-page":"42","volume-title":"Wissensbasierte System, GI-Kongrex 1985, Informatik-Fachberichte 112","author":"A. Blaser","year":"1985","unstructured":"A. Blaser, B. Alschwee, He. Lehmann, Hu. Lehmann, W. Sch\u00f6nfeld, Ein Expertensystem mit nat\u00fcrlichsprachlichem Dialog \u2014 Ein Projektbericht, in: W. Brauer, R. Radig (Hrsg.), Wissensbasierte System, GI-Kongrex 1985, Informatik-Fachberichte 112, Springer-Verlag, Berlin 1985, 42\u201357"},{"key":"18_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"W.W. Bledsoe, Non-resolution theorem proving, Artificial Intelligence 9(1977), 1\u201335","journal-title":"Artificial Intelligence"},{"key":"18_CR4","doi-asserted-by":"crossref","first-page":"473","DOI":"10.2307\/2274395","volume":"52.2","author":"W.A. Carnielli","year":"1987","unstructured":"W.A. Carnielli, Systematization of finite many-valued logics through the method of tableaux, J. Symbolic Logic 52.2 (1987), 473\u2013493","journal-title":"J. Symbolic Logic"},{"key":"18_CR5","first-page":"114","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"A.K. Chandra, D.C. Kozen, L.J. Stockmeyer, Alternation, J. ACM 28(1981), 114\u2013133","journal-title":"Alternation, J. ACM"},{"key":"18_CR6","volume-title":"Logic and data bases","author":"K. Clark","year":"1978","unstructured":"K. Clark, Negation as failure, in: H. Gallaire e.a. (eds.), Logic and data bases, Plenum Press, New York 1978"},{"unstructured":"A. Colmerauer, H. Kanoui, R. Pasero, P. Roussel, Un syst\u00e8me de communication homme-machine en fran\u00e7ais, Rapport Groupe Intelligence Artificielle, Marseille 1973.","key":"18_CR7"},{"key":"18_CR8","first-page":"167","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen, Untersuchungen \u00fcber das logische Schliessen, Math. Zeitschr. 39 (1934), 167\u2013210, 405\u2013431.","journal-title":"Math. Zeitschr."},{"key":"18_CR9","doi-asserted-by":"crossref","first-page":"14","DOI":"10.2307\/2268661","volume":"16","author":"A. Horn","year":"1951","unstructured":"A. Horn, On sentences which are true of direct unions of algebras, J. Symbolic Logic 16(1951), 14\u201321.","journal-title":"J. Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"F. Oppacher, E. Suen, Controlling deduction with proof condensation and heuristics, Proc. 8th Conf. Automated Deduction, 384\u2013393","key":"18_CR10","DOI":"10.1007\/3-540-16780-3_105"},{"key":"18_CR11","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson, A machine-oriented logic based on the resolution principle, J. ACM 12(1965), 23\u201341","journal-title":"J. ACM"},{"unstructured":"W. Sch\u00f6nfeld, PROLOG extensions based on tableau calculus, Proc. 9th Int. Conf. Artificial Intelligence, Aug. 1985, Los Angeles, Ca., Vol. 2, 730\u2013732","key":"18_CR12"},{"unstructured":"P.H. Schmitt, The THOT Theorem Prover, TR 87.09.007, IBM Wissenschaftliches Zentrum Heidelberg (1987)","key":"18_CR13"},{"key":"18_CR14","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/0743-1066(84)90021-9","volume":"1","author":"E. H. Shapiro","year":"1984","unstructured":"Ehud H. Shapiro, Alternation and the Computational Complexity of Logic Programs, J. Logic Programming 1(1984), 19\u201333","journal-title":"J. Logic Programming"},{"key":"18_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-order logic","author":"R.M. Smullyan","year":"1968","unstructured":"R.M. Smullyan, First-order logic, Springer-Verlag, Berlin-Heidelberg-New York 1968"},{"unstructured":"G. Wrightson, Semantic tableaux, unification, and links, Technical Report CSD-ANZARP-84-001, University of Wellington, 1984","key":"18_CR16"}],"container-title":["Lecture Notes in Computer Science","CSL '87"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50241-6_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T00:54:35Z","timestamp":1619571275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50241-6_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540502418","9783540459606"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-50241-6_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}