{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:30Z","timestamp":1749124050291},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"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":[[1994]]},"DOI":"10.1007\/bf00881952","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:25:12Z","timestamp":1104002712000},"page":"409-421","source":"Crossref","is-referenced-by-count":9,"title":["Tableau-based theorem provers: Systems and implementations"],"prefix":"10.1007","volume":"13","author":[{"given":"J.","family":"Schumann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Astrachan, O. L.: Investigations in Model Elimination Based Theorem Proving, PhD thesis, Duke University, 1992."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Loveland, D. W.: METEORs: High performance theorem provers using model elimination, in R. S. Boyer (ed.),Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer Academic Publishers, 1991.","DOI":"10.1007\/978-94-011-3488-0_2"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Stickel, M. E.: Caching and lemmaizing in model elimination theorem provers, in D. Kapur (ed.),Proc. CADE 11, 11th International Conference on Automated Deduction, Lecture Notes in AI, Springer, 1992, pp. 224?238.","DOI":"10.1007\/3-540-55602-8_168"},{"issue":"2","key":"CR4","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1049\/sej.1991.0006","volume":"6","author":"W. Atkinson","year":"1991","unstructured":"Atkinson, W. and Cunningham, J.: Proving properties of a safety-critical system,IEEE Software Engineering Journal 6(2) (1991), 41?50. Charles Babbage Award Paper.","journal-title":"IEEE Software Engineering Journal"},{"key":"CR5","unstructured":"Baumgartner, P.: Linear Completion: Combining the Linear and the Unit-Resulting Restrictions. Research Report 9\/93, University of Koblenz, 1993."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Baumgartner, P. and Furbach, U.: Model elimination without contrapositives, inProc. 12th International Conference on Automated Deduction, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_7"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Baumgartner, P. and Furbach, U.: PROTEIN: APROver with aTheoryExtensionInterface, in12th International Conference on Automated Deduction, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_57"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Beckert, B. and H\ufffdhnle, R.: An improved method for adding equality to free variable semantic tableau, in D. Kapur (ed.),Proc. CADE 11, 11th International Conference on Automated Deduction, Saratoga Springs, Lecture Notes in AI 607, Springer-Verlag, 1992, pp. 507?521.","DOI":"10.1007\/3-540-55602-8_188"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BF00244281","volume":"8","author":"S. Bose","year":"1992","unstructured":"Bose, S., Clarke, E. M., Long, D. E., and Michaylov, S.: Parthenon: a parallel theorem prover for non-Horn clauses,Journal of Automated Reasoning 8 (1992), 153?181.","journal-title":"Journal of Automated Reasoning"},{"key":"CR10","unstructured":"Costa, M. and Cunningham, J.: Tableaux for an action logic. Technical Report PPR1, Esprit 3125 Medlar project, 1993. (Accepted subject to revision by theJournal of Logic and Computation.)"},{"key":"CR11","unstructured":"Crawford, J. M. and Auton, L. D.: Experimental results on the crossover point in satisfiability problems, inProc. AAAI-93, 1993."},{"key":"CR12","unstructured":"Dahn, B. I.: Integration of logic functions, in J. Denzinger and J. Avenhaus (eds),Proc. of the Annual Meeting of ?GI-Fachgruppe Deduktion,? SEKI-Report SR-93-11. Universit\ufffdt Kaiserslautern, 1993."},{"key":"CR13","unstructured":"de Kogel, E. A. and Ophelders, W. M. J.: A tableaux-based automated theorem prover, in H. C. M. de Swart (ed.),LOGIC: Mathematics, Language, Computer Science and Philosophy, vol. 2, Verlag Peter Lang, 1994."},{"key":"CR14","unstructured":"de Swart, H. C. M. and Ophelders, W. M. J.: Tableaux, resolution, and complexity of formulas, inMethods of Logic in Computer Science, 1993."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Ertel, W.: OR-parallel theorem proving with random competition, inProceedings of LPAR'92, LNAI, vol. 624, Springer, 1992, pp. 226?237.","DOI":"10.1007\/BFb0013064"},{"key":"CR16","unstructured":"Gerberding, S.: DT-Ein Tableaubeweiser f\ufffdr dreiwertige Pr\ufffddikatenlogik erster Stufe. User's Manual and System Description, 1992."},{"key":"CR17","volume-title":"D\ufffdmonstration automatique en logique classique: Complexit\ufffd et m\ufffdthodes","author":"J. Goubault","year":"1993","unstructured":"Goubault, J.: D\ufffdmonstration automatique en logique classique: Complexit\ufffd et m\ufffdthodes. PhD thesis, Laboratoire d'informatique de l'Ecole Polytechnique, Ecole Polytechnique, Palaiseau, France, 1993."},{"key":"CR18","volume-title":"Syntax independent connections","author":"J. Goubault","year":"1993","unstructured":"Goubault, J.: Syntax independent connections, inProc. 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseilles, France, Max Planck-Institut f\ufffdr Informatik, Saarbr\ufffdcken, Germany, 1993."},{"key":"CR19","unstructured":"Grundy, M.: Cameo: Refutation Proving by Unordered Model Classifications. Technical Report TR-ARP-6\/90, The Australian National University, Automated Reasoning Project, 1990."},{"key":"CR20","unstructured":"Grundy, M.: Tableau Efficiency and Cameo. Technical Report TR-ARP-13\/91, The Australian National University, Automated Reasoning Project, 1991."},{"key":"CR21","unstructured":"Grundy, M.: Theorem Prover Generation Using Refutation Procedures. PhD dissertation, The University of Sydney, Basser Department of Computer Science, 1992."},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"H\ufffdhnle, R.:Automated Theorem Proving in Multiple-Valued Logics, Oxford University Press, 1993.","DOI":"10.1093\/oso\/9780198539896.001.0001"},{"key":"CR23","unstructured":"H\ufffdhnle, R., Beckert, B., Gerberding, S., and Kernig, W.: The Many-Valued Tableau-Based Theorem Prover3 T A P. Technical Report, IBM Germany Scientific Center Institute of Knowledge Based Systems, 1992."},{"key":"CR24","unstructured":"H\ufffdhnle, R. and Schmitt, P. H.: The Liberalized ?-Rule in Free Variable Semantic Tableaux. Technical Report, Universit\ufffdt Karlsruhe, Institut f\ufffdr Logik, Komplexit\ufffdt und Deduktionssysteme, 1991."},{"issue":"2","key":"CR25","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF01383880","volume":"2","author":"R. Kumar","year":"1993","unstructured":"Kumar, R., Schneider, K., and Kropf, Th.: Structuring and automating hardware proofs in a higher-order theorem-proving environment,Journal of Formal Methods in System Design,2(2) (1993), 165?230.","journal-title":"Journal of Formal Methods in System Design"},{"key":"CR26","unstructured":"Lafon, E. and Schwind, C. B.: A theorem prover for action performance, in E. Kodratoff (ed.),European Conference on Artificial Intelligence, ECAI-88, Pitman, 1988, pp. 541?546."},{"issue":"2","key":"CR27","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,Journal of Automated Reasoning 8(2) (1992), 183?212.","journal-title":"Journal of Automated Reasoning"},{"key":"CR28","volume-title":"Automated Theorem Proving: a Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.:Automated Theorem Proving: a Logical Basis, North-Holland, Amsterdam, 1978."},{"key":"CR29","first-page":"183","volume-title":"On the relative merits of path dissolution and the method of analytic tableaux (Condensed)","author":"N. Murray","year":"1993","unstructured":"Murray, N. and Rosenthal, E.: On the relative merits of path dissolution and the method of analytic tableaux (Condensed), inProc. 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseilles, France, Max Planck-Institut f\ufffdr Informatik, Saarbr\ufffdcken, Germany, 1993, pp. 183?194."},{"key":"CR30","unstructured":"Neitz, W.: A connection method-based theorem prover with selective backtracking, inProc. Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lautenbach, Germany, number TR 8\/92. Institute f\ufffdr Logik, Komplexit\ufffdt und Deduktionssysteme, Universit\ufffdt Karlsruhe, 1992."},{"key":"CR31","unstructured":"Neitz, W.: Selective backtracking in the connection method, inProc. IMYCS'92, Gorden and Breach, 1992."},{"key":"CR32","volume-title":"Automated Theorem Proving Based upon a Tableau-Method with Unification under Restrictions: Theory, Implementation and Empirical Results","author":"W. M. J. Ophelders","year":"1992","unstructured":"Ophelders, W. M. J.: Automated Theorem Proving Based upon a Tableau-Method with Unification under Restrictions: Theory, Implementation and Empirical Results. PhD thesis, Tilburg University, The Netherlands, 1992."},{"issue":"2?4","key":"CR33","doi-asserted-by":"crossref","first-page":"109","DOI":"10.3233\/FI-1993-182-403","volume":"18","author":"W. M. J. Ophelders","year":"1993","unstructured":"Ophelders, W. M. J. and de Swart, H. C. M.: Tableaux versus resolution: A comparison,Fundamenta Informaticae 18(2?4) (1993), 109?127. Special Issue: Algebraic Logic and Its Applications.","journal-title":"Fundamenta Informaticae"},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"Oppacher, S. and Suen, E.: HARP: A tableau-based theorem prover,Journal of Automated Reasoning (4) (1988), 69?100.","DOI":"10.1007\/BF00244513"},{"key":"CR35","volume-title":"Deduktion mit Shannongraphen f\ufffdr Pr\ufffddikatenlogik erster Stufe","author":"J. Posegga","year":"1993","unstructured":"Posegga, J.:Deduktion mit Shannongraphen f\ufffdr Pr\ufffddikatenlogik erster Stufe, Dissertation, Universit\ufffdt Karlsruhe, Germany, 1993."},{"key":"CR36","unstructured":"Posegga, J. and Lud\ufffdscher, B.: Towards first-order deduction based on shannon graphs, inProc. German Workshop on Artificial Intelligence (GWAI), Bonn, Germany, Lecture Notes in AI, Springer, 1992."},{"key":"CR37","volume-title":"Deduction with first-order BDDs","author":"J. Posegga","year":"1993","unstructured":"Posegga, J. and Schneider, K.: Deduction with first-order BDDs, inProc. 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseilles, France, Max Planck-Institut f\ufffdr Informatik, Saarbr\ufffdcken, Germany, 1993."},{"key":"CR38","first-page":"225","volume-title":"Experiments in computing prime implicants and prime implicates using techniques not requiring clause form","author":"A. Ramesh","year":"1993","unstructured":"Ramesh, A. and Murray, N.: Experiments in computing prime implicants and prime implicates using techniques not requiring clause form, inProc. 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseilles, France. Max Planck-Institut f\ufffdr Informatik, Saarbr\ufffdcken, Germany, 1993, pp. 225?228."},{"key":"CR39","doi-asserted-by":"crossref","unstructured":"Ramesh, A. and Murray, N.: Non-clausal deductive techniques for computing prime implicants and prime implicates, inFourth International Conference on Logic Programming and Automated Reasoning (LPAR), Lecture Notes in AI, Springer, 1993.","DOI":"10.1007\/3-540-56944-8_60"},{"key":"CR40","unstructured":"Schneider, K., Kumar, R., and Kropf, Th.: Accelerating tableaux proofs using compact representations,Journal of Formal Methods in System Design (1993)."},{"key":"CR41","unstructured":"Schneider, K., Kumar, R., and Kropf, Th.: Hardware verification with first-order BDDs, inConference on Computer Hardware Description Languages (1993)."},{"key":"CR42","doi-asserted-by":"crossref","unstructured":"Schumann, J. and Letz, R.: PARTHEO: A high-performance parallel theorem prover, inProceedings of the 10th International Conference on Automated Deduction (CADE), Lecture Notes in AI 449, Springer, 1990, pp. 40?56.","DOI":"10.1007\/3-540-52885-7_78"},{"key":"CR43","unstructured":"Schwind, C. B.: Un d\ufffdmonstrateur de th\ufffdor\ufffdmes pour des logiques modales et temporelles, en Prolog, inS\ufffdme Congr\ufffds AFCET Reconnaissances des formes et Intelligence Artificielle, Grenoble, 1985, pp. 897?913."},{"key":"CR44","doi-asserted-by":"crossref","unstructured":"Schwind, C. B.: A tableaux-based theorem prover for a decidable subset of default logic, in M. E. Stickel (ed.),Proc. CADE 10, 10th International Conference on Automated Deduction, Kaiserslautern, Germany, Lecture Notes in AI 449, Springer-Verlag, 1990, pp. 528?542.","DOI":"10.1007\/3-540-52885-7_112"},{"issue":"4","key":"CR45","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E.: A Prolog technology theorem prover: implementation by an extended prolog compiler,Journal of Automated Reasoning 4(4) (1988), 353?380.","journal-title":"Journal of Automated Reasoning"},{"key":"CR46","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0304-3975(92)90168-F","volume":"104","author":"M. E. Stickel","year":"1992","unstructured":"Stickel, M. E.: A Prolog technology theorem prover: a new exposition and implementation in prolog,Theoretical Computer Science 104 (1992), 109?128.","journal-title":"Theoretical Computer Science"},{"key":"CR47","unstructured":"Tammet, T.:Proof Search Strategies in Linear Logic, Programming Methodology Group Report 70, Chalmers University of Technology, University of G\ufffdteborg, 1993."},{"key":"CR48","unstructured":"Wallace, K.: Tableau-based automated theorem provers: the use of heuristics and software engineering techniques to increase deductive power. PhD thesis, University of Newcastle, Australia, 1994 (to appear)."},{"key":"CR49","unstructured":"Wolf, A.:Deduktionssysteme und Taktik\ufffdbersetzung, Diplomarbeit, Humboldt-Universit\ufffdt zu Berlin, Fachbereich Mathematik, 1992."},{"key":"CR50","series-title":"Technical Report CSD-ANZARP-84-001","volume-title":"Semantic Tableaux, Unification and Links","author":"G. Wrightson","year":"1984","unstructured":"Wrightson, G.:Semantic Tableaux, Unification and Links, Technical Report CSD-ANZARP-84-001, Victoria University, Wellington, New Zealand, 1984."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881952.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881952\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881952","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,17]],"date-time":"2024-01-17T10:09:25Z","timestamp":1705486165000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881952"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881952"],"URL":"https:\/\/doi.org\/10.1007\/bf00881952","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}