{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T16:13:04Z","timestamp":1779379984986,"version":"3.53.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540405245","type":"print"},{"value":"9783540450696","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45069-6_34","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T17:11:46Z","timestamp":1277226706000},"page":"355-367","source":"Crossref","is-referenced-by-count":58,"title":["Theorem Proving Using Lazy Proof Explication"],"prefix":"10.1007","author":[{"given":"Cormac","family":"Flanagan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rajeev","family":"Joshi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xinming","family":"Ou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James B.","family":"Saxe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Input files for Math-SAT case studies, \n                    \n                      http:\/\/www.dit.unitn.it\/~rseba\/Mathsat.html"},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over Boolean and linear mathematical propositions. In: Proceedings of the 18th Conference on Automated Deduction (July 2002)","DOI":"10.1007\/3-540-45620-1_17"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.: Validity checking for combinations of theories with equality. In: Proceedings of Formal Methods In Computer- Aided Design, pp. 187\u2013201 (November 1996)","DOI":"10.1007\/BFb0031808"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 236\u2013249. Springer, Heidelberg (2002)"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"1999","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 470\u2013482. Springer, Heidelberg (1999)"},{"key":"34_CR6","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Deciding CLU logic formulas via Boolean and pseudo-Boolean encodings. In: Proceedings of the First International Workshop on Constraints in Formal Verification (September 2002)"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. In: Proceedings 12th International Conference on Computer Aided Verification, pp. 85\u201398 (July 2000)","DOI":"10.1007\/10722167_10"},{"key":"34_CR9","doi-asserted-by":"publisher","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. JACM\u00a07, 201\u2013215 (1960)","journal-title":"JACM"},{"key":"34_CR10","unstructured":"de Moura, L., Ruess, H.: Lemmas on demand for satisfiability solvers. In: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (May 2002)"},{"key":"34_CR11","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: A theorem-prover for program checking. Technical report, HP Systems Research Center (2003) (in preparation)"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-36126-X_9","volume-title":"Formal Methods in Computer-Aided Design","author":"S.K. Lahiri","year":"2002","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 142\u2013159. Springer, Heidelberg (2002)"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 39th Design Automation Conference (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"34_CR14","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie-Mellon University (1998), Also available as CMU Computer Science Technical Report CMU-CS-98-154"},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: Proof generation in the Touchstone theorem prover. In: Proceedings of the 17th International Conference on Automated Deduction, pp. 25\u201344 (June 2000)","DOI":"10.1007\/10721959_3"},{"key":"34_CR16","unstructured":"Nelson, C.G.: Techniques for Program Verification. PhD thesis, Stanford University (1979), A revised version of this thesis was published as Xerox PARC Computer Science Laboratory Research Report CSL-81-10"},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. JACM\u00a027(2) (October 1979)","DOI":"10.1145\/322186.322198"},{"issue":"2","key":"34_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"Silva, J.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5) (May 1999)","DOI":"10.1109\/12.769433"},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Strichman, O.: On solving Presburger and linear arithmetic with SAT. In: Proceedings Formal Methods in Computer-Aided Design, pp. 160\u2013170 (2002)","DOI":"10.1007\/3-540-36126-X_10"},{"issue":"3","key":"34_CR21","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1137\/0213035","volume":"13","author":"R.E. Tarjan","year":"1984","unstructured":"Tarjan, R.E., Yannakakis, M.: Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM Journal of Computing\u00a013(3), 566\u2013579 (1984)","journal-title":"SIAM Journal of Computing"},{"key":"34_CR22","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of the 14th International Conference on Automated Deduction, pp. 272\u2013275 (1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"34_CR23","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: Proceedings of the International Conference on Computer Aided Design (November 2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45069-6_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,30]],"date-time":"2020-01-30T11:12:38Z","timestamp":1580382758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45069-6_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405245","9783540450696"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45069-6_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}