{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:20:53Z","timestamp":1725484853925},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_33","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T05:24:41Z","timestamp":1180675481000},"page":"493-507","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Finding Tractable Formulas in NNF"],"prefix":"10.1007","author":[{"given":"Edgar","family":"Altamirano","sequence":"first","affiliation":[]},{"given":"Gon\u00e7al","family":"Escalada-Imaz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"issue":"1","key":"33_CR1","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1080\/11663081.1995.10510841","volume":"5","author":"G. Aguilera","year":"1995","unstructured":"Aguilera, G., de Guzman, I.P., Ojeda, M.: Increasing the efficiency of automated theorem proving. Journal of Applied Non-classical Logics, 5:1 (1995) 9\u201329","journal-title":"Journal of Applied Non-classical Logics"},{"key":"33_CR2","unstructured":"Altamirano, E., Escalada-Imaz G.: Efficient algorithms for several factorized Horn theories (in Spanish). 2nd Congress Catala d\u2019Intel.ligencia Artificial, Girona, Spain (1999) 31\u201338"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Andrews, P.B.: Theorem proving via general matings. Journal of Association Computing Machinery, 28 (1981)","DOI":"10.1145\/322248.322249"},{"key":"33_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0196-6774(80)90007-3","volume":"1","author":"B. Aspvall","year":"1980","unstructured":"Aspvall, B.: Recognising disguised NR(1) instances of the satisfiability problem. Journal of Algorithms, 1 (1980) 97\u2013103","journal-title":"Journal of Algorithms"},{"issue":"3","key":"33_CR5","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall B., Plass M.F., Tarjan R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters, 8:3 (1979) 121\u2013132","journal-title":"Information Processing Letters"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated theorem proving. Fiedr, Vieweg and Sohn. (1982)","DOI":"10.1007\/978-3-322-90100-2"},{"key":"33_CR7","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel W.: Mating in matrices. Communications of the ACM, 26:11 (1983)","journal-title":"Communications of the ACM"},{"key":"33_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1137\/S0097539792228629","volume":"23","author":"E. Boros","year":"1994","unstructured":"Boros E., Crama Y., Hammer P.L., Saks M.: A complexity index for satisfiability problems SIAM Journal on Computing, 23 (1994) 45\u201349","journal-title":"SIAM Journal on Computing"},{"key":"33_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0166-218X(94)90033-7","volume":"55","author":"E. Boros","year":"1994","unstructured":"Boros E., Hammer P.L., Sun X.: Recognition of q-Horn formulae in linear time. Discrete Applied Mathematics, 55 (1994) 1\u201313","journal-title":"Discrete Applied Mathematics"},{"key":"33_CR10","unstructured":"Boy de la Tour, T.: Minimising the number of clauses by renaming. In: CADE-10, (1990) 558\u2013572"},{"key":"33_CR11","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/102782.102789","volume":"38","author":"V. Chandru","year":"1991","unstructured":"Chandru V., Hooker, J.N.: Extended Horn sets in propositional logic. Journal of ACM, 38 (1991) 205\u2013221","journal-title":"Journal of ACM"},{"key":"33_CR12","unstructured":"Cook S.A.: The complexity of theorem-proving procedures. Third ACM Symposium on theory of Computing, (1971) 151\u2013158"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Conforti M., Cornu\u00e9jols G., Kapoor A., Vuskovi\u0107 K., Rao M.R.: Balanced matrices. In: J.R. Birge and K.G. Murty, Mathematical Programming: State of the Art, (1994)","DOI":"10.21236\/ADA280021"},{"key":"33_CR14","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W.F. Dowling","year":"1984","unstructured":"Dowling W.F., Gallier J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 3 (1984) 267\u2013284","journal-title":"Journal of Logic Programming"},{"key":"33_CR15","unstructured":"Escalada-Imaz G.: Optimisation d\u2019algorithmes d\u2019inference monotone en logique des propositions et du premier ordre. Universit\u00e9 Paul Sabatier, Toulouse, France (1989)"},{"key":"33_CR16","unstructured":"Escalada-Imaz G.: Linear forward inferences engines for a class of rule systems (in French). Laboratoire D\u2019Automatique et Analyse des Systemes, Toulouse, France, (1989) LAAS-89172"},{"key":"33_CR17","unstructured":"Escalada-Imaz G.: A quadratic algorithm and a linear algorithm for 2-CNF (in French). Laboratoire D\u2019Automatique et Analyse des Systemes, Toulouse, France, (1989) LAAS-89378"},{"issue":"3","key":"33_CR18","first-page":"23","volume":"27","author":"G. Escalada-Imaz","year":"1994","unstructured":"Escalada-Imaz G., Mart\u00ednez-Enr\u00edquez A.M.: Forward chaining inference engines of optimal complexity for several classes of rule based systems (in Spanish). Inform\u00e1tica y Autom\u00e1tica, 27:3 (1994) 23\u201330","journal-title":"Inform\u00e1tica y Autom\u00e1tica"},{"key":"33_CR19","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1137\/0205048","volume":"5","author":"S. Even","year":"1976","unstructured":"Even S., Itai A., Shamir A.: On the complexity of timetable and multicommodity flow problems. SIAM J. of Computing, 5 (1976) 691\u2013703","journal-title":"SIAM J. of Computing"},{"key":"33_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0743-1066(91)90015-H","volume":"11","author":"M. Ghallab","year":"1991","unstructured":"Ghallab M., Escalada-Imaz, G.: A linear control algorithm for a class of rule-based systems. Journal of Logic Programming, 11 (1991) 117\u2013132","journal-title":"Journal of Logic Programming"},{"key":"33_CR21","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0743-1066(89)90009-5","volume":"7","author":"G. Gallo","year":"1989","unstructured":"Gallo, G., Urbani, G.: Algorithms for testing the satisfiability of propositional formulae. Journal of Logic Programming, 7 (1989) 45\u201361","journal-title":"Journal of Logic Programming"},{"issue":"6","key":"33_CR22","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1093\/logcom\/4.6.905","volume":"4","author":"R. H\u00e4hnle","year":"1994","unstructured":"H\u00e4hnle, R.: Short conjunctive normal forms in finitely-valued logics. Journal of Logic and Computation, 4:6 (1994) 905\u2013927","journal-title":"Journal of Logic and Computation"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle R., Murray N.V., Rosenthal, E.: Completeness for linear regular negation normal form inference systems. In: Proceedings ISMIS\u201997, (1997)","DOI":"10.1007\/3-540-63614-5_57"},{"issue":"4","key":"33_CR24","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/321850.321857","volume":"21","author":"L. Henschen","year":"1974","unstructured":"Henschen L., Wos L.: Unit refutations and Horn sets. Journal of the Association for Computing Machinery, 21:4 (1974) 590\u2013605","journal-title":"Journal of the Association for Computing Machinery"},{"key":"33_CR25","first-page":"30","volume":"72","author":"L. Henschen","year":"1980","unstructured":"Henschen L., Lusk E., Overbeek R., Smith B.T., Veroff R., Winker S., Wos L.: Challenge problem 1. SIGART Newsletter, 72 (1980) 30\u201331","journal-title":"SIGART Newsletter"},{"key":"33_CR26","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0304-3975(76)90068-2","volume":"3","author":"N. Jones","year":"1977","unstructured":"Jones N., Laaser W.: Complete problems for deterministic polynomial time. Theoretical Computer Science, 3 (1977) 105\u2013117","journal-title":"Theoretical Computer Science"},{"key":"33_CR27","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Complexity of Computer Computations","author":"R.M. Karp","year":"1972","unstructured":"Karp R.M.: Reducibility among combinatorial problems. In: Miller, R. E., Thatcher, J. W. (eds): Complexity of Computer Computations. Plenum Press. N.Y. (1972) 85\u2013103"},{"key":"33_CR28","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H.R. Lewis","year":"1978","unstructured":"Lewis H.R.: Renaming a set of clauses as a Horn set. Journal of the ACM, 25 (1978) 134\u2013135","journal-title":"Journal of the ACM"},{"key":"33_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","volume":"29","author":"M. Minoux","year":"1988","unstructured":"Minoux, M.: LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation. Information Processing Letters, 29 (1988) 1\u201312","journal-title":"Information Processing Letters"},{"key":"33_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","volume-title":"Proc. COLOG-88","author":"G. Mints","year":"1990","unstructured":"Mints, G.: Gentzen-type systems and resolution rules, part 1: Propositional logic. In: Proc. COLOG-88, Tallin. Lecture Notes in Computer Science, 417. Springer, (1990) 198\u2013231"},{"key":"33_CR31","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/174130.174135","volume":"3","author":"N.V. Murray","year":"1993","unstructured":"Murray N.V., Rosenthal, E.: Dissolution: making paths vanish. Journal of the ACM, 3 (1993) 504\u2013535","journal-title":"Journal of the ACM"},{"key":"33_CR32","unstructured":"Ramesh, A.G.: Some applications of non-Clausal deduction. Department of Computer Science, State University of new York at Albany, (1995)"},{"key":"33_CR33","unstructured":"Roy, R., Chowdhury, Dalal: Model theoretic semantics and tractable algorithm for CNF-BCP, In: Proc. of the AAAI-97, (1997) 227\u2013232"},{"key":"33_CR34","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0743-1066(90)90026-2","volume":"8","author":"M.G. Scutell\u00e0","year":"1990","unstructured":"Scutell\u00e0 M.G.: A note on Dowling and Gallier\u2019s top-down algorithm for propositional Horn satisfiability. Journal of Logic Programming, 8 (1990) 265\u2013273","journal-title":"Journal of Logic Programming"},{"key":"33_CR35","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0020-0190(95)00019-9","volume":"54","author":"J.S. Schlipf","year":"1995","unstructured":"Schlipf J.S., Annextein F., Franco J., Swaminathan, R.P.: On finding solutions for extended Horn formulas. Information Processing Letters, 54 (1995) 133\u2013137","journal-title":"Information Processing Letters"},{"key":"33_CR36","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00249017","volume":"7","author":"R. Socher","year":"1991","unstructured":"Socher, R.: Optimising the clausal normal form transformation. Journal of Automated Reasoning, 7 (1991) 325\u2013336","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/BFb0055921","volume-title":"International Conference on Artificial Intelligence and Symbolic Computation","author":"Z. Stachniak","year":"1998","unstructured":"Stachniak, Z.: Non-clausal reasoning with propositional definite theories. In: International Conference on Artificial Intelligence and Symbolic Computation. Lecture Notes in Computer Science, 1476. Springer Verlag, (1998) 296\u2013307"},{"key":"33_CR38","unstructured":"Stachniak, Z.: Polarity guided tractable reasoning. In: International American Association on Artificial Intelligence, AAAI-99 (1999) 751\u2013758"},{"key":"33_CR39","unstructured":"Tseitin, G.: On the complexity of proofs in propositional logics. In: Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning 2: Classical Papers on Computational Logic, Springer, (1983) 466\u2013483"}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:31:03Z","timestamp":1558272663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_33","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"15 December 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}