{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T11:39:00Z","timestamp":1648985940274},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"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":[[1993]]},"DOI":"10.1007\/bf00881867","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:34:31Z","timestamp":1104132871000},"page":"115-136","source":"Crossref","is-referenced-by-count":1,"title":["Simplification in a satisfiability checker for VLSI applications"],"prefix":"10.1007","volume":"10","author":[{"given":"Frank","family":"Vlach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","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 (Second edition), Vieweg Verlag, Braunschweig (1987).","edition":"Second edition"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244489","volume":"6","author":"W. Bibel","year":"1990","unstructured":"Bibel, W., ?Short proofs of the pigeonhole formulas based on the connection method?,J. Automated Reasoning 6, 287?298 (1990).","journal-title":"J. Automated Reasoning"},{"key":"CR3","unstructured":"Boole, G.,An Investigation of The Laws of Thought, 1854. Reprint. Dover Publications. No place or date."},{"key":"CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-2821-6","volume-title":"Logic Minimization Algorithms for VLSI Synthesis","author":"R. K. Brayton","year":"1984","unstructured":"Brayton, R. K., Hachtel, G. D., McMullen, C. T., and Sangiovanni-Vincentelli, A.,Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, Boston (1984)."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E., ?Graph-based algorithms for Boolean function manipulation?,IEEE Trans. on Computers C-35, 667?691 (August, 1986).","journal-title":"IEEE Trans. on Computers"},{"key":"CR6","unstructured":"Burch, J. R.,et al., ?Symbolic model checking: 1020 states and beyond?,Proceedings Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 428?439 (1990)."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"916","DOI":"10.2307\/2273826","volume":"52","author":"S. R. Buss","year":"1987","unstructured":"Buss, S. R., ?Polynomial size proofs of the propositional pigeonhole principle?,J. Symbolic Logic 52, 916?927 (1987).","journal-title":"J. Symbolic Logic"},{"key":"CR8","volume-title":"Formal VLSI Correctness Verification: VLSI Design Methods ? II (Proceedings IFIP WG 10.2\/WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design)","year":"1990","unstructured":"Claesen, L. (ed.),Formal VLSI Correctness Verification: VLSI Design Methods ? II (Proceedings IFIP WG 10.2\/WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design). North-Holland, Amsterdam (1990)."},{"key":"CR9","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1145\/1008335.1008338","volume":"8","author":"S. A. Cook","year":"1976","unstructured":"Cook, S. A., ?A short proof of the pigeon hole principle using extended resolution?,ACM SIGACT News 8, 28?32 (1976).","journal-title":"ACM SIGACT News"},{"key":"CR10","doi-asserted-by":"crossref","DOI":"10.3792\/chmm\/1263313783","volume-title":"The Algebra of Logic","author":"L. Couturat","year":"1914","unstructured":"Couturat, L.,The Algebra of Logic. Open Court, Chicago (1914)."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M. and Putnam, H., ?A computing procedure for quantification theory?,J. ACM 7, 201?215 (1960).","journal-title":"J. ACM"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Fujita, M., Fujisawa, H., and Kawato, N., ?Evaluation and improvements of Boolean comparison methods based on binary decision diagrams?,Proc. ICCAD, 2?5 (1988).","DOI":"10.1109\/ICCAD.1988.122450"},{"key":"CR13","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Michael R. Garey","year":"1979","unstructured":"Garey, Michael R. and Johnson, David S.,Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, New York (1979)."},{"key":"CR14","doi-asserted-by":"crossref","first-page":"616","DOI":"10.1109\/43.3200","volume":"7","author":"G. D. Hachtel","year":"1988","unstructured":"Hachtel, G. D. and Jacoby, R. M., ?Verification algorithms for VLSI synthesis?,IEEE Trans. Computer-Aided Design 7, 616?640 (May, 1988).","journal-title":"IEEE Trans. Computer-Aided Design"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A., ?The intractability of resolution?,Theor. Computer Sci. 39, 297?308 (1985).","journal-title":"Theor. Computer Sci."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1142\/S0218001487000102","volume":"1","author":"R. M. Haralick","year":"1987","unstructured":"Haralick, R. M. and Wu, S.-H., ?An approximate linear time propagate and divide theorem prover for propositional logic?,Int. J. Pattern Recognition, Artificial Intelligence 1, 141?155 (April, 1987).","journal-title":"Int. J. Pattern Recognition, Artificial Intelligence"},{"key":"CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-349-15428-9","volume-title":"Metalogic: An Introduction to the Metatheory of Standard First Order Logic","author":"G. Hunter","year":"1971","unstructured":"Hunter, G.,Metalogic: An Introduction to the Metatheory of Standard First Order Logic. University of California Press, Berkeley (1971)."},{"key":"CR18","first-page":"119","volume-title":"Formal VLSI Correctness Verification: VLSI Design Methods ? II (Proceedings IFIP WG 10.2\/WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design)","author":"J. C. Madre","year":"1990","unstructured":"Madre, J. C., ?Benchmarks for tautology checking ? experimental results?, in [8], pp. 119?124."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Malik, S., Wang, A. R., Brayton, R. K., and Sangiovanni-Vincentelli, A., ?Logic verification using binary decision diagrams in a logic synthesis environment?,Proc. ICCAD, pp. 6?9 (1988).","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"CR20","volume-title":"Methods of Logic","author":"W. V. O. Quine","year":"1950","unstructured":"Quine, W. V. O.,Methods of Logic. Holt, Rinehart, Winston, New York (1950)."},{"key":"CR21","volume-title":"Logic: Form and Function","author":"J. A. Robinson","year":"1979","unstructured":"Robinson, J. A.,Logic: Form and Function. North-Holland, New York (1979)."},{"key":"CR22","first-page":"2646","volume":"15","author":"J. P. Roth","year":"1973","unstructured":"Roth, J. P., ?VERIFY: An algorithm to verify a computer design?,IBM Tech. Disclosure Bull. 15, 2646?2648 (1973).","journal-title":"IBM Tech. Disclosure Bull."},{"key":"CR23","volume-title":"Computer Logic, Testing, and Verification","author":"J. P. Roth","year":"1980","unstructured":"Roth, J. P.,Computer Logic, Testing, and Verification. Computer Science Press, Potomac, Md (1980)."},{"key":"CR24","first-page":"713","volume":"57","author":"C. E. Shannon","year":"1938","unstructured":"Shannon, C. E., ?A symbolic analysis of relay and switching circuits?,Trans. AIEE 57, 713?719 (1938).","journal-title":"Trans. AIEE"},{"key":"CR25","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1147\/rd.261.0106","volume":"26","author":"G. L. Smith","year":"1982","unstructured":"Smith, G. L., Bahnsen, J., and Halliwell, H., ?Boolean comparison of hardware and flowcharts?,IBM Res. Dev. 26, 106?116 (1982).","journal-title":"IBM Res. Dev."},{"key":"CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-13394-1","volume-title":"Proceedings 7th International Conference on Automated Deduction","author":"A. Gelder Van","year":"1984","unstructured":"Van Gelder, A., ?A satisfiability tester for non-clausal propositional calculus?,Proceedings 7th International Conference on Automated Deduction (Lecture Notes in Computer Science, Vol. 170). Springer-Verlag, New York (1984)."},{"key":"CR27","first-page":"89","volume-title":"Formal VLSI Correctness Verification: VLSI Design Methods ? II (Proceedings IFIP WG 10.2\/WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design)","author":"F. Vlach","year":"1990","unstructured":"Vlach, F., ?A note on the INSTEP tautology checker and the IFIP and ISCAS benchmarks?, in [8], pp. 89?94."},{"key":"CR28","unstructured":"Vlach, F., ?A tautology checker for VLSI applications that uses rule-based simplification and directed backtracking?, Technical Report N-90-0010, Department of Computer Science, University of North Texas, 1990."},{"key":"CR29","volume-title":"The Complexity of Boolean Functions","author":"Ingo Wegener","year":"1987","unstructured":"Wegener, Ingo,The Complexity of Boolean Functions. Wiley, New York (1987)."},{"key":"CR30","unstructured":"Wei, R.-S. and Sangiovanni-Vincentelli, A., ?PROTEUS: A logic verification system for combinational circuits?, inProceedings 1986 IEEE International Test Conference, pp. 350?358."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881867.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881867\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881867","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,2]],"date-time":"2021-07-02T15:46:04Z","timestamp":1625240764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881867"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881867"],"URL":"https:\/\/doi.org\/10.1007\/bf00881867","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}