{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:11:47Z","timestamp":1725459107556},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601166"},{"type":"electronic","value":"9783540494430"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0035972","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T10:13:56Z","timestamp":1138184036000},"page":"389-398","source":"Crossref","is-referenced-by-count":1,"title":["Using classical theorem-proving techniques for approximate reasoning: Revised report"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Br\u00fcning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Torsten","family":"Schaub","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"40_CR1","unstructured":"M. Cadoli. Semantical and computational aspects of horn approximations. In Proc. of IJCAI, pages 39\u201345, 1993."},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"M. Cadoli and M. Schaerf. Approximate Entailment. In Proc. of the Conf. of the Ital. Ass. for AI, pages 68\u201377. Springer, 1991.","DOI":"10.1007\/3-540-54712-6_219"},{"key":"40_CR3","unstructured":"C. Chang. The decomposition principle for theorem proving systems. In Allerton Conf. on Circuit and System Theory, pages 20\u201328, U. of Illinois, 1972."},{"key":"40_CR4","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W. P. Dowling","year":"1984","unstructured":"W. P. Dowling and J. P. Gallier. Linear-time algorithms for testing the satisfiability of propositional horn formulae. Jour. of Logic Programming, 1:267\u2013284, 1984.","journal-title":"Jour. of Logic Programming"},{"key":"40_CR5","unstructured":"M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, 1979."},{"key":"40_CR6","unstructured":"H. Kautz and B. Selman. Forming Concepts for Fast Inference. In Proc. of AAAI, 1992."},{"key":"40_CR7","unstructured":"H. Kautz and B. Selman. An empirical evaluation of knowledge compilation. In Proc. of AAAI, 1994."},{"key":"40_CR8","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/BF00297511","volume":"17","author":"H. Levesque","year":"1988","unstructured":"H. Levesque. Logic and the complexity of reasoning. Jour. of Phil. Logic, 17:355\u2013389, 1988.","journal-title":"Jour. of Phil. Logic"},{"issue":"1","key":"40_CR9","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H. R. Lewis","year":"1978","unstructured":"H. R. Lewis. Renaming a Set of Clauses as a Horn Set. Jour. of the ACM, 25(1):134\u2013135, 1978.","journal-title":"Jour. of the ACM"},{"key":"40_CR10","unstructured":"W. McCune. Otter users' guide. Argonne Nat'l Laboratories, Argonne, 1988."},{"key":"40_CR11","unstructured":"G. Neugebauer. From Horn Clauses to First Order Logic: A Graceful Ascent. Technical Report AIDA-92-21, TH Darmstadt, 1992."},{"key":"40_CR12","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. Automatic deduction with hyper-resolution. Jour. of Computer Math., 1:227\u2013234, 1965.","journal-title":"Jour. of Computer Math."},{"key":"40_CR13","unstructured":"B. Selman and H. Kautz. Knowlede Compilation Using Horn Approximations. In Proc. of AAAI, 1991."},{"key":"40_CR14","unstructured":"L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning, Introduction and Applications. Prentice-Hall, 1984."}],"container-title":["Lecture Notes in Computer Science","Advances in Intelligent Computing \u2014 IPMU '94"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0035972","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,9]],"date-time":"2019-02-09T03:49:33Z","timestamp":1549684173000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0035972"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601166","9783540494430"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0035972","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}