{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:18:32Z","timestamp":1725491912243},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730989"},{"type":"electronic","value":"9783540730996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73099-6_16","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T07:04:02Z","timestamp":1189753442000},"page":"199-215","source":"Crossref","is-referenced-by-count":0,"title":["A Bottom-Up Approach to Clausal Tableaux"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Peltier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Logics in Artificial Intelligence","author":"P. Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper-tableaux. In: Or\u0142owska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol.\u00a01126, Springer, Heidelberg (1996)"},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0747-7171(03)00026-9","volume":"36","author":"B. Beckert","year":"2003","unstructured":"Beckert, B.: Depth-first proof search without backtracking for free-variable clausal tableaux. Journal of Symbolic Computation\u00a036, 117\u2013138 (2003)","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"Beckert, B., Posegga, J.: Lean-TAP: Lean tableau-based deduction. Journal of Automated Reasoning\u00a015(3), 339\u2013358 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR4","unstructured":"Benoist, E., H\u00e9brard, J.J.: Ordered formulas. Technical Report\u00a014, Universit\u00e9 de Caen, Les cahiers du CGREYC (1999)"},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On matrices with connections. Journal of the Association of Computing Machinery\u00a028, 633\u2013645 (1981)","journal-title":"Journal of the Association of Computing Machinery"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61363-3","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The disconnection method: a confluent integration of unification in the analytic framework. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, Springer, Heidelberg (1996)"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF01531068","volume":"1","author":"E. Boros","year":"1990","unstructured":"Boros, E., Crama, Y., Hammer, P.L.: Polynomial-time inference of all valid implications for Horn and related formulae. Ann. Mathematics and Artificial Intelligence\u00a01, 21\u201332 (1990)","journal-title":"Ann. Mathematics and Artificial Intelligence"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"F. Bry","year":"1996","unstructured":"Bry, F., Yahya, A.: Minimal model generation with positive unit hyper-resolution tableaux. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, Springer, Heidelberg (1996)"},{"issue":"1","key":"16_CR9","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. J. ACM\u00a038(1), 205\u2013221 (1991)","journal-title":"J. ACM"},{"key":"16_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_46","volume-title":"Automated Reasoning","author":"M. Giese","year":"2001","unstructured":"Giese, M.: Incremental Closure of Free Variable Tableaux. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, Springer, Heidelberg (2001)"},{"key":"16_CR11","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, Elsevier Science vol. I, ch. 3, pp. 100\u2013178 (2001)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures, pp. 2015\u20132112 (2001)","DOI":"10.1016\/B978-044450813-3\/50030-8"},{"key":"16_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, Springer, Heidelberg (2001)"},{"key":"16_CR14","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Logics in Artificial Intelligence","author":"N. Peltier","year":"2004","unstructured":"Peltier, N.: Some techniques for branch-saturation in free-variable tableaux. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, Springer, Heidelberg (2004)"},{"issue":"3","key":"16_CR15","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., Annexstein, F.S., Franco, J.V., Swaminathan, R.P.: On Finding Solutions for Extended Horn Formulas. Information Processing Letters\u00a054(3), 133\u2013137 (1995)","journal-title":"Information Processing Letters"},{"issue":"3","key":"16_CR16","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0166-218X(93)E0170-4","volume":"59","author":"R.P. Swaminathan","year":"1995","unstructured":"Swaminathan, R.P., Wagner, D.K.: The arborescence-realization problem. Discrete Appl. Math\u00a059(3), 267\u2013283 (1995)","journal-title":"Discrete Appl. Math"},{"key":"16_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0019-9958(83)80027-8","volume":"59","author":"S. Yamasaki","year":"1983","unstructured":"Yamasaki, S., Doshita, S.: The satisfiability problem for a class consisting of Horn sentences and some non-Horn sentences in propositional logic. Information and Control\u00a059, 1\u201312 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:59Z","timestamp":1619517599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730989","9783540730996"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}