{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T03:40:14Z","timestamp":1735530014389,"version":"3.32.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1994,7,1]],"date-time":"1994-07-01T00:00:00Z","timestamp":773020800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1994,7]]},"DOI":"10.1007\/bf01384237","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T02:09:32Z","timestamp":1112407772000},"page":"145-176","source":"Crossref","is-referenced-by-count":3,"title":["Accelerating tableaux proofs using compact representations"],"prefix":"10.1007","volume":"5","author":[{"given":"Klaus","family":"Schneider","sequence":"first","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1992","unstructured":"Gupta, A., ?Formal hardware verification methods: A survey,?Journal of Formal Methods in System Design, 1:151?238, 1992.","journal-title":"Journal of Formal Methods in System Design"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Lindstr\u00f6m, J., ?On extensions of elementary logic,?Theoria, 35, 1969.","DOI":"10.1111\/j.1755-2567.1969.tb00356.x"},{"key":"CR3","unstructured":"Gordon, M.J.C., ?Why higher-order logic is a good formalism for specifying and verifying hardware,? in G. Milne and P.A. Subrahmanyam, editors,Formal aspects of VLSI Design. North-Holand, 1986."},{"issue":"3","key":"CR4","first-page":"242","volume":"133","author":"F.K. Hanna","year":"1986","unstructured":"Hanna, F.K. and Daeche, N., ?Specification and verification of digital systems using higher-order predicate logic,?IEE Proc. Pt. E, 133(3):242?254, 1986.","journal-title":"IEE Proc. Pt. E"},{"key":"CR5","unstructured":"Joyce, J., ?More reasons why higher-order logic is a good formalism for specifying and verifying hardware,? inInternational Workshop on formal Methods in VLSI Design, Miami, 1991."},{"issue":"2","key":"CR6","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 System Design, 2(2):165?230, 1993.","journal-title":"Journal of Formal System Design"},{"key":"CR7","series-title":"number 607 in Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"766","DOI":"10.1007\/3-540-55602-8_221","volume-title":"11th Conference on Automated Deduction","author":"K. Schneider","year":"1992","unstructured":"Schneider, K., Kumar, R. and Kropf, Th., ?The FAUST prover,? in D. Kapur, editor,11th Conference on Automated Deduction, number 607 in Lecture Notes in Computer Science, 766?770, Springer Verlag, Albany, New York, 1992."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"1","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G., ?Untersuchungen \u00fcber das logisches Schlie\u00dfen,?Mathematische Zeitschrift, 1:176?210, 1935.","journal-title":"Mathematische Zeitschrift"},{"issue":"2","key":"CR9","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B., ?Refutations by matings,?Journal of the ACM, 28(2):193?214, April 1981.","journal-title":"Journal of the ACM"},{"issue":"11","key":"CR10","doi-asserted-by":"crossref","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel, W., ?Matings and matrices,?Communications of the ACM, 26(11):844?852, 1983.","journal-title":"Communications of the ACM"},{"key":"CR11","unstructured":"Ebbinghaus, H.D., Flum, J. and Thomas, W.,Einf\u00fchrung in die mathematische Logik, Wissenschaftliche Buchgesellschaft Darmstadt, 1978."},{"key":"CR12","unstructured":"Shoenfield, J.R.,Mathematical Logic, Addison-Wesley, 1967."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Fitting, M.,First-Order Logic and Automated Theorem Proving, Springer Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Fitting, M.,Proof Methods for Modal and Intuitionistic Logic, Reidel Publishing Company, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Eder, E.,On the relative complexities of first order calculi, Vieweg Verlag, 1991.","DOI":"10.1007\/978-3-322-84222-0"},{"issue":"3","key":"CR16","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/BF00156916","volume":"1","author":"M. d. Agostino","year":"1992","unstructured":"Agostino, M. d., ?Are Tableaux an Improvement of Truth-Tables? Cut-Free Proofs and Bivalence,?Journal of Logic, Language, and Information, 1(3):127?139, 1992.","journal-title":"Journal of Logic, Language, and Information"},{"issue":"1","key":"CR17","first-page":"23","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A., ?A machine oriented logic based on the resolution principle,?Journal of Automated Reasoning, 12(1):23?41, 1965.","journal-title":"Journal of Automated Reasoning"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M.S. Paterson","year":"1978","unstructured":"Paterson, M.S. and Wegman, M.N., ?Linear unification,?Journal of Computer and System Sciences, 16:181?186, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A. and Monanari, M., ?An efficient unification algorithm,?ACM TOPLAS, 4:258?282, 1982.","journal-title":"ACM TOPLAS"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0022-0000(86)90003-6","volume":"32","author":"D. Champeaux de","year":"1986","unstructured":"Champeaux, D. de, About the Paterson-Wegman unification algorithm,Journal of Computer and System Sciences, 32:79?90, 1986.","journal-title":"Journal of Computer and System Sciences"},{"key":"CR21","unstructured":"Corbin, J. and Bidoit, M., ?A rehabilitation of Robinson's unification algorithm,?Information Processing, pages 909?914, 1983."},{"issue":"13","key":"CR22","first-page":"309","volume":"18","author":"E.W. Beth","year":"1955","unstructured":"Beth, E.W., ?Semantic entailment and formal derivability,?Medlingen der Koninklijke Nederlandse Akademic van Wetenschapen, 18(13):309?342, 1955.","journal-title":"Medlingen der Koninklijke Nederlandse Akademic van Wetenschapen"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.,First Order Logic, Springer Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M.C. Fitting","year":"1988","unstructured":"Fitting, M.C., ?First-order modal tableaux,?Journal of Automated Reasoning, 4:191?213, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"CR25","unstructured":"Broda, K.,The Application of Semantic Tableaux with Unification to Automated Deduction. Ph.D thesis, Department of Computing, Imperial College, 1991."},{"key":"CR26","unstructured":"Posegga, J. and Schneider, K., ?Deduction with first-order BDDs,?Internal report, Max-Planck-Institut f\u00fcr Informatik, 1993. Proc. of Second Workshop on Theorem Proving with analytic Tableaux and Related Methods."},{"key":"CR27","unstructured":"Schneider, K., Kumar, R. and Kropf, Th., ?Hardware verification with first-order BDD's? inConference on Computer Hardware Dscription Languages, 1993."},{"key":"CR28","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.?Journal of Automated Reasoning, 2:191?216, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"Kumar, R., Kropf, Th. and Schneider, K., ?Integrating a first-order automatic prover in the HOL environment,? inInternational Workshop on the HOL Theorem Proving System and its Applications, pages 170?176. IEEE Press, 1991.","DOI":"10.1109\/HOL.1991.596284"},{"key":"CR30","unstructured":"H\u00e4hnle, R. and Schmitt, P., ?The liberalized ?-rule,?Journal of Automated Reasoning, 1993."},{"issue":"4","key":"CR31","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"Kowalski, R., ?A proof procedure using connection graphs,?Journal of the ACM, 22(4):572?595, 1975.","journal-title":"Journal of the ACM"},{"key":"CR32","unstructured":"Wrightson, G., ?Semantic tableaux with links,? inAI'87 Conference, 1987."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384237.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384237\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384237","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T02:36:19Z","timestamp":1735526179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384237"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,7]]},"references-count":32,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1994,7]]}},"alternative-id":["BF01384237"],"URL":"https:\/\/doi.org\/10.1007\/bf01384237","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1994,7]]}}}