{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:40:16Z","timestamp":1725518416562},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_33","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"380-395","source":"Crossref","is-referenced-by-count":0,"title":["Canonical Inference for Implicational Systems"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nachum","family":"Dershowitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"33_CR1","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of the ACM\u00a041(2), 236\u2013276 (1994)","journal-title":"Journal of the ACM"},{"key":"33_CR2","unstructured":"Bertet, K., Monjardet, B.: The multiple facets of the canonical direct implicational basis. Cahiers de la Maison des Sciences Economiques b05052, Universit\u00e9 Paris Panth\u00e9on-Sorbonne (June 2005), \n                      \n                        http:\/\/ideas.repec.org\/p\/mse\/wpsorb\/b05052.html"},{"key":"33_CR3","first-page":"315","volume":"6","author":"K. Bertet","year":"2004","unstructured":"Bertet, K., Nebut, M.: Efficient algorithms on the Moore family associated to an implicational system. Discrete Mathematics and Theoretical Computer Science\u00a06, 315\u2013338 (2004)","journal-title":"Discrete Mathematics and Theoretical Computer Science"},{"issue":"1","key":"33_CR4","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1145\/1182613.1182619","volume":"8","author":"M.P. Bonacina","year":"2007","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic\u00a08(1), 180\u2013208 (2007)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1 & 2","key":"33_CR5","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0743-1066(92)90050-D","volume":"14","author":"M.P. Bonacina","year":"1992","unstructured":"Bonacina, M.P., Hsiang, J.: On rewrite programs: Semantics and relationship with Prolog. Journal of Logic Programming\u00a014(1 & 2), 155\u2013180 (1992)","journal-title":"Journal of Logic Programming"},{"key":"33_CR6","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","volume":"146","author":"M.P. Bonacina","year":"1995","unstructured":"Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoretical Computer Science\u00a0146, 199\u2013242 (1995)","journal-title":"Theoretical Computer Science"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Caspard, N., Monjardet, B.: The lattice of Moore families and closure operators on a finite set: A survey. Electronic Notes in Discrete Mathematics\u00a02 (1999)","DOI":"10.1016\/S1571-0653(04)00013-7"},{"key":"33_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_2","volume-title":"Automated Reasoning","author":"A. Darwiche","year":"2006","unstructured":"Darwiche, A.: Searching while keeping a trace: the evolution from satisfiability to knowledge compilation. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130. Springer, Heidelberg (2006)"},{"issue":"2\/3","key":"33_CR9","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/S0019-9958(85)80003-6","volume":"64","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N.: Computing with rewrite systems. Information and Control\u00a064(2\/3), 122\u2013157 (1985)","journal-title":"Information and Control"},{"key":"33_CR10","unstructured":"Dershowitz, N., Huang, G.-S., Harris, M.A.: Enumeration problems related to ground Horn theories, \n                      \n                        http:\/\/arxiv.org\/pdf\/cs.LO\/0610054"},{"key":"33_CR11","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 243\u2013320. Elsevier, Amsterdam (1990)"},{"issue":"4","key":"33_CR12","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1137\/0217039","volume":"17","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Marcus, L., Tarlecki, A.: Existence, uniqueness, and construction of rewrite systems. SIAM Journal of Computing\u00a017(4), 629\u2013639 (1988)","journal-title":"SIAM Journal of Computing"},{"issue":"3","key":"33_CR13","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.F. Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formul\u00e6. Journal of Logic Programming\u00a01(3), 267\u2013284 (1984)","journal-title":"Journal of Logic Programming"},{"key":"33_CR14","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"U. Furbach","year":"2007","unstructured":"Furbach, U., Obermaier, C.: Knowledge compilation for description logics. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, Springer, Heidelberg (2007)"},{"key":"33_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.2307\/2268661","volume":"16","author":"A. Horn","year":"1951","unstructured":"Horn, A.: On sentences which are true of direct unions of algebras. Journal of Symbolic Logic\u00a016, 14\u201321 (1951)","journal-title":"Journal of Symbolic Logic"},{"key":"33_CR16","doi-asserted-by":"publisher","first-page":"61","DOI":"10.2307\/2268172","volume":"8","author":"J.C.C. McKinsey","year":"1943","unstructured":"McKinsey, J.C.C.: The decision problem for some classes of sentences without quantifiers. Journal of Symbolic Logic\u00a08, 61\u201376 (1943)","journal-title":"Journal of Symbolic Logic"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/3-540-63104-6_17","volume-title":"Automated Deduction - CADE-14","author":"O. Roussel","year":"1997","unstructured":"Roussel, O., Mathieu, P.: Exact knowledge compilation in predicate calculus: the partial achievement case. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 161\u2013175. Springer, Heidelberg (1997)"},{"key":"33_CR18","unstructured":"Sloane, N.J.A.: The On-Line Encyclopedia of Integer Sequences (1996-2006), \n                      \n                        http:\/\/www.research.att.com\/~njas\/sequences"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:36:33Z","timestamp":1620016593000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}