{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T13:39:25Z","timestamp":1648820365040},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2006,12,2]],"date-time":"2006-12-02T00:00:00Z","timestamp":1165017600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,2,28]]},"DOI":"10.1007\/s10817-006-9048-8","type":"journal-article","created":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T11:49:39Z","timestamp":1164973779000},"page":"79-126","source":"Crossref","is-referenced-by-count":4,"title":["The Disconnection Tableau Calculus"],"prefix":"10.1007","volume":"38","author":[{"given":"Reinhold","family":"Letz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Stenz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,12,2]]},"reference":[{"key":"9048_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem proving through general matings. J. Assoc. Comput. Mach. 28, 193\u2013214 (1981)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9048_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-79351-6","volume-title":"Reduktionssysteme","author":"J. Avenhaus","year":"1995","unstructured":"Avenhaus, J.: Reduktionssysteme. Springer, Berlin Heidelberg New York (1995)"},{"key":"9048_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"9048_CR4","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures, vol. 2","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Ait-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 1\u201330. Academic, New York (1989)"},{"issue":"3","key":"9048_CR5","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"key":"9048_CR6","first-page":"353","volume-title":"Automated Deduction: A Basis for Applications. Foundations: Calculi and Methods, vol. 1","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmidt, P.H. (eds.) Automated Deduction: A Basis for Applications Foundations: Calculi and Methods, vol. 1, pp. 353\u2013398. Kluwer, Dordrecht, The Netherlands (1998)"},{"key":"9048_CR7","first-page":"60","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands. Lecture Notes in Computer Science, vol. 1397","author":"P. Baumgartner","year":"1998","unstructured":"Baumgartner, P.: Hyper Tableaux \u2013 the next generation. In: de Swart, H. (ed.) Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands. Lecture Notes in Computer Science, vol. 1397, pp. 60\u201376. Springer, Berlin Heidelberg New York (1998)"},{"key":"9048_CR8","first-page":"200","volume-title":"Proceedings of the 17th International Conference on Automated Deduction (CADE-17), Pittsburgh. Lecture Notes in Artificial Intelligence, vol. 1831","author":"P. Baumgartner","year":"2000","unstructured":"Baumgartner, P.: FDPLL \u2013 A first-order Davis\u2013Putnam\u2013Logeman\u2013Loveland procedure. In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction (CADE-17), Pittsburgh. Lecture Notes in Artificial Intelligence, vol. 1831, pp. 200\u2013219. Springer, Berlin Heidelberg New York (2000)"},{"key":"9048_CR9","first-page":"329","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE), Trento, Italy. Lecture Notes in Computer Science, vol. 1632","author":"P. Baumgartner","year":"1999","unstructured":"Baumgartner, P., Eisinger, N., Furbach, U.: A confluent connection calculus. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction (CADE), Trento, Italy. Lecture Notes in Computer Science, vol. 1632, pp. 329\u2013343. Springer, Berlin Heidelberg New York (1999)"},{"key":"9048_CR10","first-page":"1","volume-title":"Proceedings of the European JELIA Workshop (JELIA-96): Logics in Artificial Intelligence. Lecture Notes in Artificial Intelligence, vol. 1126","author":"P. Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds.) Proceedings of the European JELIA Workshop (JELIA-96): Logics in Artificial Intelligence. Lecture Notes in Artificial Intelligence, vol. 1126, pp. 1\u201317. Springer, Berlin Heidelberg New York (1996)"},{"key":"9048_CR11","first-page":"350","volume-title":"Automated Deduction \u2013 CADE-19. Lecture Notes in Artificial Intelligence, vol. 2741","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) Automated Deduction \u2013 CADE-19. Lecture Notes in Artificial Intelligence, vol. 2741, pp. 350\u2013364. Springer, Berlin Heidelberg New York (2003)"},{"key":"9048_CR12","first-page":"392","volume-title":"CADE-20 \u2013 The 20th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 3632","author":"P. Baumgartner","year":"2005","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus with equality. In: Nieuwenhuis, R. (ed.) CADE-20 \u2013 The 20th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 3632, pp. 392\u2013408. Springer, Berlin Heidelberg New York (2005)"},{"key":"9048_CR13","first-page":"265","volume-title":"Automated Deduction \u2013 A Basis for Applications. Foundations, vol. 1","author":"B. Beckert","year":"1998","unstructured":"Beckert, B.: Rigid E-unification. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction \u2013 A Basis for Applications. Foundations, vol. 1, pp. 265\u2013289. Kluwer, Dordrecht, The Netherlands (1998)"},{"key":"9048_CR14","doi-asserted-by":"crossref","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. J. Symb. Comput. 36, 117\u2013138 (2003)","journal-title":"J. Symb. Comput."},{"key":"9048_CR15","first-page":"758","volume-title":"Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY. Lecture Notes in Computer Science, vol. 607","author":"B. Beckert","year":"1992","unstructured":"Beckert, B., Gerberding, S., H\u00e4hnle, R., Kernig, W.: The tableau-based theorem prover $_{3}{T}^{{{A}}}{P}$ for multiple-valued logics. In: Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY. Lecture Notes in Computer Science, vol. 607, pp. 758\u2013760. Springer, Berlin Heidelberg New York (1992)"},{"key":"9048_CR16","first-page":"11","volume-title":"Automated Deduction \u2013 A Basis for Applications. Foundations, vol. 1","author":"B. Beckert","year":"1998","unstructured":"Beckert, B., H\u00e4hnle, R.: Analytic tableaux. In: Automated Deduction \u2013 A Basis for Applications. Foundations, vol. 1, pp. 11\u201341. Kluwer, Dordrecht, The Netherlands (1998)"},{"issue":"3","key":"9048_CR17","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"Beckert, B., Posegga, J.: leanTAP: lean tableau-based deduction. J. Autom. Reason. 15(3), 339\u2013358 (1995)","journal-title":"J. Autom. Reason."},{"issue":"13","key":"9048_CR18","first-page":"309","volume":"18","author":"E.W. Beth","year":"1955","unstructured":"Beth, E.W.: Semantic entailment and formal derivability. Meded. K. Ned. Akad. Wet. 18(13), 309\u2013342 (1955)","journal-title":"Meded. K. Ned. Akad. Wet."},{"key":"9048_CR19","doi-asserted-by":"crossref","unstructured":"Bibel, W.: On matrices with connections. J. Assoc. Comput. Mach. 633\u2013645 (1981)","DOI":"10.1145\/322276.322277"},{"key":"9048_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg-Verlag, Braunschweig, Germany (1987)(revised)","edition":"2"},{"key":"9048_CR21","first-page":"110","volume-title":"Proceedings, 5th TABLEAUX. Lecture Notes in Artificial Intelligence, vol. 1","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The disconnection method: a confluent integration of unification in the analytic framework. In: Proceedings, 5th TABLEAUX. Lecture Notes in Artificial Intelligence, vol. 1, pp. 110\u2013126. Springer, Berlin Heidelberg New York (1996)"},{"issue":"4","key":"9048_CR22","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4(4), 412\u2013430 (1975)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"9048_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01355585","volume":"3","author":"J. Cohen","year":"1974","unstructured":"Cohen, J., Trilling, L., Wegner, P.: A nucleus of a theorem-prover described in ALGOL-68. Int. J. Comput. Inf. Sci. 3(1), 1\u201331 (1974)","journal-title":"Int. J. Comput. Inf. Sci."},{"key":"9048_CR24","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"9048_CR25","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. Assoc. Comput. Mach. 7(3), 201\u2013215 (1960)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9048_CR26","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1016\/B978-044450813-3\/50011-4","volume-title":"Handbook of Automated Reasoning, vol. 1","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz, N., Plaisted, D.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 535\u2013610. Elsevier, Amsterdam, The Netherlands (2001)(Chapt.\u00a09)"},{"key":"9048_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M.C. Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Berlin Heidelberg New York (1996)(revised)","edition":"2"},{"key":"9048_CR28","first-page":"55","volume-title":"Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), Los Alamitos, CA, vol. 9","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), Los Alamitos, CA, vol. 9, pp. 55\u201364. IEEE Computer Society, Washington, DC (2003)"},{"key":"9048_CR29","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Math. Z. 39, 176\u2013210, 405\u2013431 (1935) (English translation) In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North Holland, Amsterdam, The Netherlands (1969)","DOI":"10.1007\/BF01201363"},{"key":"9048_CR30","unstructured":"Giese, M.: Model generation style completeness proofs for constraint tableaux with superposition. Technical Report 2001-20, Institut f\u00fcr Logik, Komplexit\u00e4t und Deduktionssysteme, Universit\u00e4t Karlsruhe, Germany (2001)"},{"key":"9048_CR31","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-3-540-45206-5_8","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Rome, Italy. Lecture Notes in Computer Science, vol. 2796","author":"M. Giese","year":"2003","unstructured":"Giese, M.: Simplification rules for constrained formula tableaux. In: Mayer, M.C., Pirri, F. (eds.) Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Rome, Italy. Lecture Notes in Computer Science, vol. 2796, pp. 65\u201380. Springer, Berlin Heidelberg New York (2003)"},{"issue":"5","key":"9048_CR32","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"J. Hooker","year":"2002","unstructured":"Hooker, J., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first-order logic. J. Autom. Reason. 28(5), 371\u2013396 (2002)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9048_CR33","first-page":"25","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Lee, S.-J., Plaisted, D.: Eliminating duplication with the hyper-linking strategy. J. Autom. Reason. 9(1), 25\u201342 (1992)","journal-title":"J. Autom. Reason."},{"key":"9048_CR34","unstructured":"Letz, R.: First-order calculi and proof procedures for automated deduction. Ph.D. Thesis, Technieche Hochschule, Darmstadt (1993)"},{"key":"9048_CR35","first-page":"123","volume-title":"Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI), France, Chambery","author":"R. Letz","year":"1993","unstructured":"Letz, R.: On the polynomial transparency of resolution. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI), France, Chambery, pp. 123\u2013129. Morgan Kaufmann, San Mateo, CA (1993)"},{"issue":"2","key":"9048_CR36","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1005839531398","volume":"18","author":"R. Letz","year":"1997","unstructured":"Letz, R.: LINUS: a link instantiation prover with unit support. J. Autom. Reason. 18(2), 205\u2013210 (1997)","journal-title":"J. Autom. Reason."},{"key":"9048_CR37","first-page":"43","volume-title":"Automated Deduction \u2013 A Basis for Applications. Foundations, vol. 1","author":"R. Letz","year":"1998","unstructured":"Letz, R.: Clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction \u2013 A Basis for Applications. Foundations, vol. 1, pp. 43\u201372. Kluwer, Dordrecht, The Netherlands (1998)"},{"key":"9048_CR38","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-94-017-1754-0_3","volume-title":"Handbook of Tableau Methods","author":"R. Letz","year":"1999","unstructured":"Letz, R.: First-order tableaux methods. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 125\u2013196. Kluwer, Dordrecht, The Netherlands (1999)"},{"issue":"3","key":"9048_CR39","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection Tableau calculi. J. Autom. Reason. 13(3), 297\u2013338 (1994)","journal-title":"J. Autom. Reason."},{"key":"9048_CR40","first-page":"381","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001), Siena, Italy. Lecture Notes in Artificial Intelligence, vol. 2083","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: DCTP: a disconnection calculus theorem prover. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001), Siena, Italy. Lecture Notes in Artificial Intelligence, vol. 2083, pp. 381\u2013385. Springer, Berlin Heidelberg New York (2001)"},{"key":"9048_CR41","first-page":"142","volume-title":"Proceedings of the 8th LPAR, Havanna, Cuba, vol. 2250","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Voronkov, A. (ed.) Proceedings of the 8th LPAR, Havanna, Cuba, vol. 2250, pp. 142\u2013156. Springer, Berlin Heidelberg New York (2001)"},{"key":"9048_CR42","first-page":"176","volume-title":"Proceedings, TABLEAUX-2002, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2381","author":"R. Letz","year":"2002","unstructured":"Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Proceedings, TABLEAUX-2002, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2381, pp. 176\u2013190. Springer, Berlin Heidelberg New York (2002)"},{"key":"9048_CR43","first-page":"289","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2004), Cork, Ireland. Lecture Notes in Artificial Intelligence, vol. 3097","author":"R. Letz","year":"2004","unstructured":"Letz, R., Stenz, G.: Generalised handling of variables in disconnection tableaux. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2004), Cork, Ireland. Lecture Notes in Artificial Intelligence, vol. 3097, pp. 289\u2013306. Springer, Berlin Heidelberg New York (2004)"},{"key":"9048_CR44","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction (CADE), Argonne, IL, vol. 310","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) 9th International Conference on Automated Deduction (CADE), Argonne, IL, vol. 310, pp. 415\u2013434. Springer, Berlin Heidelberg New York (1988)"},{"key":"9048_CR45","first-page":"217","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands, vol. 1397","author":"F. Massacci","year":"1998","unstructured":"Massacci, F.: Simplification: a general constraint propagation technique for propositional and modal tableaux. In: de Swart, H. (ed.) Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands, vol. 1397, pp. 217\u2013231. Springer, Berlin Heidelberg New York (1998)"},{"key":"9048_CR46","unstructured":"Moser, M.: Goal-directed reasoning in clausal logic with equality. Ph.D. Thesis, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany (1996)"},{"issue":"2","key":"9048_CR47","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., Mayr, K.: SETHEO and E-SETHEO \u2013 the CADE-13 systems. J. Autom. Reason. 18(2), 237\u2013246 (1997)","journal-title":"J. Autom. Reason."},{"key":"9048_CR48","unstructured":"Moser, M., Steinbach, J.: STE-modification revisited. AR-Report AR-97-03, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1997)"},{"key":"9048_CR49","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning, vol. 1","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 371\u2013443. Elsevier, Amsterdam, The Netherlands (2001)(Chapt.\u00a07)"},{"issue":"3\u20134","key":"9048_CR50","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W. Nutt","year":"1989","unstructured":"Nutt, W., R\u00e9ty, P., Smolka, G.: Basic narrowing revisited. J. Symb. Comput. 7(3\u20134), 295\u2013318 (1989)","journal-title":"J. Symb. Comput."},{"key":"9048_CR51","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"Oppacher, F., Suen, E.: HARP: a tableau-based theorem prover. J. Autom. Reason. 4, 69\u2013100 (1988)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9048_CR52","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D.A. Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reason. 25(3), 167\u2013217 (2000)","journal-title":"J. Autom. Reason."},{"key":"9048_CR53","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"Prawitz, D.: An improved proof procedure. Theoria 26, 102\u2013139 (1960) (Reprinted in [58])","journal-title":"Theoria"},{"key":"9048_CR54","first-page":"285","volume-title":"Automation of Reasoning, 1983","author":"D. Prawitz","year":"1969","unstructured":"Prawitz, D.: Advances and problems in mechanical proof procedures. In: Automation of Reasoning, 1983, pp. 285\u2013297. Springer, Berlin Heidelberg New York (1969) (reprinted)"},{"key":"9048_CR55","doi-asserted-by":"crossref","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 23\u201341 (1965)","DOI":"10.1145\/321250.321253"},{"key":"9048_CR56","first-page":"280","volume-title":"Proceedings of the 18th CADE, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2392","author":"S. Schulz","year":"2002","unstructured":"Schulz, S., Sutcliffe, G.: System description: GrAnDe 1.0. In: Voronkov, A. (ed.) Proceedings of the 18th CADE, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2392, pp. 280\u2013284. Springer, Berlin Heidelberg New York (2002)"},{"key":"9048_CR57","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R.E. Shostak","year":"1976","unstructured":"Shostak, R.E.: Refutation graphs. Artif. Intell. 7, 51\u201364 (1976)","journal-title":"Artif. Intell."},{"key":"9048_CR58","volume-title":"Automation of Reasoning","year":"1983","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning. Springer, Berlin Heidelberg New York (1983) (Two volumes)"},{"key":"9048_CR59","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-order logic","author":"R. Smullyan","year":"1968","unstructured":"Smullyan, R.: First-order logic. Springer, Berlin Heidelberg New York (1968)"},{"key":"9048_CR60","first-page":"335","volume-title":"Proceedings of TABLEAUX-2002, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2381","author":"G. Stenz","year":"2002","unstructured":"Stenz, G.: DCTP 1.2 \u2013 system abstract. In: Proceedings of TABLEAUX-2002, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2381, pp. 335\u2013340. Springer, Berlin Heidelberg New York (2002)"},{"key":"9048_CR61","unstructured":"Stenz, G.: The disconnection calculus. Dissertation, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Logos Verlag, Berlin (2002)"},{"key":"9048_CR62","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of proofs in propositional logics. Semin. Math. 8, (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"9048_CR63","first-page":"272","volume-title":"Proceedings of the 14th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 1249","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: an efficient propositional prover. In: McCune, W. (ed.) Proceedings of the 14th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 1249, pp. 272\u2013275. Springer, Berlin Heidelberg New York (1997)"},{"key":"9048_CR64","unstructured":"Zhang, H., Stickel, M.E.: An efficient algorithm for unit propagation. In: Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH\u201996), pp. 166\u2013169. Fort Lauderdale, FL (1996)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9048-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9048-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9048-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:47Z","timestamp":1559265707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9048-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12,2]]},"references-count":64,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2007,2,28]]}},"alternative-id":["9048"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9048-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12,2]]}}}