{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T06:28:29Z","timestamp":1768458509276,"version":"3.49.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"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":[[1995]]},"DOI":"10.1007\/bf00881804","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:42:21Z","timestamp":1104133341000},"page":"339-358","source":"Crossref","is-referenced-by-count":95,"title":["leanTAP: Lean tableau-based deduction"],"prefix":"10.1007","volume":"15","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Posegga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","series-title":"Techical Report","volume-title":"2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods","author":"D. Basin","year":"1993","unstructured":"Basin, D., Fronh\u00f6fer, B., H\u00e4hnle, R., Posegga, J., and Schwind, C.: 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Techical Report 213, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, May 1993."},{"key":"CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/3-540-55602-8_188","volume-title":"11th Int. Conf. on Automated Deduction (CADE)","author":"B. Heckert","year":"1992","unstructured":"Heckert, B. and H\u00e4hnle, R.: An improved method for adding equality to free variable semantic tableaux, in D. Kapur (ed.),11th Int. Conf. on Automated Deduction (CADE), Lecture Notes in Computer Science, Springer-Verlag, Albany, NY, 1992, pp. 507?521."},{"key":"CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1007\/3-540-55602-8_219","volume-title":"11th Int. Conf. on Automated Deducation (CADE)","author":"B. Beckert","year":"1992","unstructured":"Beckert, B., Gerberding, S., H\u00e4hnle, R., and Kernig, W.: The tableau-based theorem prover3 T A P for multiple-valued logics, in11th Int. Conf. on Automated Deducation (CADE), Lecture Notes in Computer Science, Springer-Verlag, Albany, NY, 1992, pp. 758?760."},{"key":"CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/BFb0022559","volume-title":"3rd Kurt G\u00f6del Colloquium (KGC)","author":"B. Beckert","year":"1993","unstructured":"Beckert, B., H\u00e4hnle, R., and Schmitt, P. H.: The even more liberalized ?-rule in free variable semantic tableaux, in G. Gottlob, A. Leitsch, and D. Mundici (eds),3rd Kurt G\u00f6del Colloquium (KGC), Lecture Notes in Computer Science, Springer-Verlag, Brno, Czech Republic, 1993, pp. 108?119."},{"key":"CR5","series-title":"Technical Report","volume-title":"3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods","author":"K. Broda","year":"1994","unstructured":"Broda, K., D'Agostino, M., Gor\u00e9, R., Johnson, R., and Reeves, S.: 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Technical Report TR-94\/5, Imperial College London, Department of Computing, London, England, April 1994."},{"key":"CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-84222-0","volume-title":"Relative Complexities of First-Order Calculi","author":"E. Eder","year":"1992","unstructured":"Eder, E.:Relative Complexities of First-Order Calculi. Artificial Intelligence. Vieweg-Verlag, 1992."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Fitting, M. C.:First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"CR8","series-title":"Technical Report","volume-title":"Workshop on Theorem Proving with Analytic Tableaux and Related Methods","author":"B. Fronh\u00f6fer","year":"1992","unstructured":"Fronh\u00f6fer, B., H\u00e4hnle, R., and K\u00e4ufl, T.: Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Technical Report 8\/92, Universit\u00e4t Karlsruhe, Fakult\u00e4t f\u00fcr Informatik, Karlsruhe, Germany, March 1992."},{"key":"CR9","unstructured":"Hilbert, D. and Bernays, P.:Grundlagen der Mathematik II, Vol. 50 of Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Ber\u00fccksichtigung der Anwendungsgebiete, Springer-Verlag, 1939."},{"key":"CR10","unstructured":"K\u00e4ufl, T. and Zabel, N.: Cooperation of decision procedures in a tableau-based theorem prover,Revude d'Intelligence Artificielle 4(3) (1990)."},{"issue":"2","key":"CR11","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., and Bibel, W.: SETHEO: A high-performance theorem prover,J. Automated Reasoning 8(2) (1992), 183?212.","journal-title":"J. Automated Reasoning"},{"key":"CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th Int. Conf. on Automated Deducation (CADE)","author":"R. Manthey","year":"1988","unstructured":"Manthey, R. and Bry, F.: SATCHMO: A theorem power implemented in Prolog, in E. Lusk and R. Overbeek (eds),9th Int. Conf. on Automated Deducation (CADE), Lecture Notes in Computer Science, Springer-Verlag, Argonne, IL, 1988, pp. 415?434."},{"key":"CR13","series-title":"Technical Report","volume-title":"Otter 2.0 Users Guide","author":"W. W. McCune","year":"1990","unstructured":"McCune, W. W.: Otter 2.0 Users Guide, Technical Report ANL-90\/9, Argonne National Laboratory, Mathematics and Computer Science Division, Argonne, IL, March 1990."},{"key":"CR14","unstructured":"O'Keefe, R. A.:The Craft of Prolog, MIT Press, 1990."},{"key":"CR15","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"Oppacher, F. and Suen, E.: HARP: A tableau-based theorem prover,J. Automated Reasoning 4 (1988), 69?100.","journal-title":"J. Automated Reasoning"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J.: Seventy-five problems for testing automatic theorem provers,J. Automated Reasoning 2 (1986), 191?216.","journal-title":"J. Automated Reasoning"},{"key":"CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BFb0018993","volume-title":"7th Int. Symp. on Methodologies for Intelligent Systems (ISMIS)","author":"J. Posegga","year":"1993","unstructured":"Posegga, J.: Compiling proof search in semantic tableaux, in7th Int. Symp. on Methodologies for Intelligent Systems (ISMIS), Lecture Notes in Computer Science, Springer-Verlag, Trondheim, Norway, 1993, pp. 67?77."},{"key":"CR18","volume-title":"Deduktion mit Shannongraphen f\u00fcr Pr\u00e4dikatenlogik erster Stufe","author":"J. Posegga","year":"1993","unstructured":"Posegga, J.:Deduktion mit Shannongraphen f\u00fcr Pr\u00e4dikatenlogik erster Stufe, Infix-Verlag, St. Augustin, Germany, 1993."},{"issue":"1?2","key":"CR19","first-page":"102","volume":"7","author":"D. Prawitz","year":"1960","unstructured":"Prawitz, D., Prawitz, H., and Voghera, N.: A mechanical proof procedure and its realization in an electronic computer,ACM 7(1?2) (1960) 102?128.","journal-title":"ACM"},{"key":"CR20","series-title":"Technical Report","volume-title":"The THOT Theorem Prover","author":"P. H. Schmitt","year":"1987","unstructured":"Schmitt, P. H.: The THOT Theorem Prover, Technical Report 87.9.7, IBM Germany, Scientific Center, Heidelberg, Germany, 1987."},{"key":"CR21","unstructured":"Sch\u00f6nfeld, W.: Prolog extensions based on tableau calculus, in9th Int. Joint Conf. on Artificial Intelligence, Los Angeles, Vol. 2, 1985, pp. 730?733."},{"key":"CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1007\/BFb0012881","volume-title":"9th Int. Conf. on Automated Deducation (CADE)","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E.: A Prolog technology theorem prover, in E. Lusk and R. Overbeek (eds),9th Int. Conf. on Automated Deducation (CADE), Lecture Notes in Computer Science, Springer-Verlag, Argonne, IL, 1988, pp. 752?753."},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Wang, H.: Toward mechanical mathematics,IBM J. Research and Development 4(1) (1960).","DOI":"10.1147\/rd.41.0002"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881804.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881804\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881804","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T12:58:10Z","timestamp":1556542690000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881804"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF00881804"],"URL":"https:\/\/doi.org\/10.1007\/bf00881804","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}