{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:34:56Z","timestamp":1750307696634,"version":"3.41.0"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003407","name":"Ministero dell'Istruzione, dell'Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","award":["2003-097383"],"award-info":[{"award-number":["2003-097383"]}],"id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,1]]},"abstract":"<jats:p>\n            Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the\n            <jats:italic>satisfiability<\/jats:italic>\n            of sets of\n            <jats:italic>ground literals<\/jats:italic>\n            in theory\n            <jats:italic>T<\/jats:italic>\n            . If a sound and complete inference system for first-order logic is guaranteed to\n            <jats:italic>terminate<\/jats:italic>\n            on\n            <jats:italic>T-satisfiability problems<\/jats:italic>\n            , any theorem-proving strategy with that system and a fair search plan is a\n            <jats:italic>T-satisfiability procedure<\/jats:italic>\n            . We prove termination of a rewrite-based first-order engine on the theories of\n            <jats:italic>records<\/jats:italic>\n            ,\n            <jats:italic>integer offsets<\/jats:italic>\n            ,\n            <jats:italic>integer offsets modulo<\/jats:italic>\n            and\n            <jats:italic>lists<\/jats:italic>\n            . We give a\n            <jats:italic>modularity theorem<\/jats:italic>\n            stating sufficient conditions for termination on a\n            <jats:italic>combination of theories<\/jats:italic>\n            , given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both\n            <jats:italic>parametric<\/jats:italic>\n            synthetic benchmarks to test\n            <jats:italic>scalability<\/jats:italic>\n            , and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.\n          <\/jats:p>","DOI":"10.1145\/1459010.1459014","type":"journal-article","created":{"date-parts":[[2009,1,29]],"date-time":"2009-01-29T13:48:36Z","timestamp":1233236916000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":60,"title":["New results on rewrite-based satisfiability procedures"],"prefix":"10.1145","volume":"10","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Genova, Genova, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria Paola","family":"Bonacina","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Verona, Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[{"name":"LORIA &amp; INRIA-Lorraine, Villers-l\u00e8s-Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Verona, Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,1,23]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 6th International Conference on Formal Engineering Methods. J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science","volume":"3308","author":"Arkoudas K.","unstructured":"Arkoudas , K. , Zee , K. , Kuncak , V. , and Rinard , M . 2004. Verifying a file system implementation . In Proceedings of the 6th International Conference on Formal Engineering Methods. J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science , vol. 3308 . Springer-Verlag, Berlin, Germany, 373--390. Arkoudas, K., Zee, K., Kuncak, V., and Rinard, M. 2004. Verifying a file system implementation. In Proceedings of the 6th International Conference on Formal Engineering Methods. J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science, vol. 3308. Springer-Verlag, Berlin, Germany, 373--390."},{"volume-title":"Notes 2nd VERIFY Workshop, FLoC. Tech. rep. 07\/2002 DIKU","author":"Armando A.","key":"e_1_2_1_2_1","unstructured":"Armando , A. , Bonacina , M. P. , Ranise , S. , Rusinowitch , M. , and Sehgal , A. K . 2002. High-performance deduction for verification: A case study in the theory of arrays . In Notes 2nd VERIFY Workshop, FLoC. Tech. rep. 07\/2002 DIKU , University of Copenhagen, Copenhagen, Denmark, 103--112. Armando, A., Bonacina, M. P., Ranise, S., Rusinowitch, M., and Sehgal, A. K. 2002. High-performance deduction for verification: A case study in the theory of arrays. In Notes 2nd VERIFY Workshop, FLoC. Tech. rep. 07\/2002 DIKU, University of Copenhagen, Copenhagen, Denmark, 103--112."},{"volume-title":"Notes 3rd PDPAR Workshop, CAV-17","author":"Armando A.","key":"e_1_2_1_3_1","unstructured":"Armando , A. , Bonacina , M. P. , Ranise , S. , and Schulz , S . 2005a. Big proof engines as little proof engines: New results on rewrite-based satisfiability procedures . In Notes 3rd PDPAR Workshop, CAV-17 . 33--41. Armando, A., Bonacina, M. P., Ranise, S., and Schulz, S. 2005a. Big proof engines as little proof engines: New results on rewrite-based satisfiability procedures. In Notes 3rd PDPAR Workshop, CAV-17. 33--41."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence","volume":"3717","author":"Armando A.","unstructured":"Armando , A. , Bonacina , M. P. , Ranise , S. , and Schulz , S . 2005b. On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal . In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence , vol. 3717 . Springer-Verlag, Berlin, Germany, 65--80. Armando, A., Bonacina, M. P., Ranise, S., and Schulz, S. 2005b. On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 65--80."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00020-8"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence","volume":"3717","author":"Baader F.","unstructured":"Baader , F. and Ghilardi , S . 2005. Connecting many-sorted structures and theories through adjoint functions . In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence , vol. 3717 . Springer-Verlag, Berlin, Germany, 31--47. Baader, F. and Ghilardi, S. 2005. Connecting many-sorted structures and theories through adjoint functions. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 31--47."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000009518.26415.49"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 16th International Conference on Computer-Aided Verification. R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science","volume":"3114","author":"Barrett C. W.","unstructured":"Barrett , C. W. and Berezin , S . 2004. CVC lite: A new implementation of the cooperating validity checker . In Proceedings of the 16th International Conference on Computer-Aided Verification. R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science , vol. 3114 . Springer-Verlag, Berlin, Germany, 515--518. Barrett, C. W. and Berezin, S. 2004. CVC lite: A new implementation of the cooperating validity checker. In Proceedings of the 16th International Conference on Computer-Aided Verification. R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 515--518."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the CADE-17","volume":"1831","author":"Barrett C. W.","unstructured":"Barrett , C. W. , Dill , D. L. , and Stump , A . 2000. A framework for cooperating decision procedures . In Proceedings of the CADE-17 , D. McAllester, Ed. Lecture Notes in Artificial Intelligence , vol. 1831 . Springer-Verlag, Berlin, Germany, 79--97. Barrett, C. W., Dill, D. L., and Stump, A. 2000. A framework for cooperating decision procedures. In Proceedings of the CADE-17, D. McAllester, Ed. Lecture Notes in Artificial Intelligence, vol. 1831. Springer-Verlag, Berlin, Germany, 79--97."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 14th International Conference on Computer-Aided Verification, K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science","volume":"2404","author":"Barrett C. W.","unstructured":"Barrett , C. W. , Dill , D. L. , and Stump , A . 2002a. Checking satisfiability of first-order formulas by incremental translation to SAT . In Proceedings of the 14th International Conference on Computer-Aided Verification, K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science , vol. 2404 . Springer-Verlag, Berlin, Germany, 236--249. Barrett, C. W., Dill, D. L., and Stump, A. 2002a. Checking satisfiability of first-order formulas by incremental translation to SAT. In Proceedings of the 14th International Conference on Computer-Aided Verification, K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany, 236--249."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 4th International Workshop on Frontiers of Combining Systems, A. Armando, Ed. Lecture Notes in Computer Science","volume":"2309","author":"Barrett C. W.","unstructured":"Barrett , C. W. , Dill , D. L. , and Stump , A . 2002b. A generalization of Shostak's method for combining decision procedures . In Proceedings of the 4th International Workshop on Frontiers of Combining Systems, A. Armando, Ed. Lecture Notes in Computer Science , vol. 2309 . Springer-Verlag, Berlin, Germany. Barrett, C. W., Dill, D. L., and Stump, A. 2002b. A generalization of Shostak's method for combining decision procedures. In Proceedings of the 4th International Workshop on Frontiers of Combining Systems, A. Armando, Ed. Lecture Notes in Computer Science, vol. 2309. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"A taxonomy of theorem-proving strategies","author":"Bonacina M. P.","unstructured":"Bonacina , M. P. 1999. A taxonomy of theorem-proving strategies . In Artificial Intelligence Today\u2014Recent Trends and Developments, M. J. Wooldridge and M. Veloso, Eds. Lecture Notes in Artificial Intelligence , vol. 1600 . Springer-Verlag , Berlin, Germany , 43--84. Bonacina, M. P. 1999. A taxonomy of theorem-proving strategies. In Artificial Intelligence Today\u2014Recent Trends and Developments, M. J. Wooldridge and M. Veloso, Eds. Lecture Notes in Artificial Intelligence, vol. 1600. Springer-Verlag, Berlin, Germany, 43--84."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182619"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.11.042"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.11.039"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the IJCAR-3, U. Furbach and N. Shankar, Eds. Lecture Notes in Artificial Intelligence","volume":"4130","author":"Bonacina M. P.","unstructured":"Bonacina , M. P. , Ghilardi , S. , Nicolini , E. , Ranise , S. , and Zucchelli , D . 2006. Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures . In Proceedings of the IJCAR-3, U. Furbach and N. Shankar, Eds. Lecture Notes in Artificial Intelligence , vol. 4130 . Springer-Verlag, Berlin, Germany, 513--527. Bonacina, M. P., Ghilardi, S., Nicolini, E., Ranise, S., and Zucchelli, D. 2006. Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In Proceedings of the IJCAR-3, U. Furbach and N. Shankar, Eds. Lecture Notes in Artificial Intelligence, vol. 4130. Springer-Verlag, Berlin, Germany, 513--527."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00187-N"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_34"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9004-z"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 14th International Conference in Computer-Aided Verification, K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science","volume":"2404","author":"Bryant R. E.","unstructured":"Bryant , R. E. , Lahiri , S. K. , and Seshia , S. A . 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions . In Proceedings of the 14th International Conference in Computer-Aided Verification, K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science , vol. 2404 . Springer-Verlag, Berlin, Germany, 78--92. Bryant, R. E., Lahiri, S. K., and Seshia, S. A. 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proceedings of the 14th International Conference in Computer-Aided Verification, K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany, 78--92."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371364"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Caferra R. Leitsch A. and Peltier N. 2004. Automated Model Building. Kluwer Academic Publishers.  Caferra R. Leitsch A. and Peltier N. 2004. Automated Model Building. Kluwer Academic Publishers.","DOI":"10.1007\/978-1-4020-2653-9"},{"key":"e_1_2_1_23_1","volume-title":"-T","author":"Chang C.-L.","year":"1973","unstructured":"Chang , C.-L. and Lee , R. C . -T . 1973 . Symbolic Logic and Mechanical Theorem Proving. Academic Press . Chang, C.-L. and Lee, R. C.-T. 1973. Symbolic Logic and Mechanical Theorem Proving. Academic Press."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for Constitution and Analysis of Systems, H. Garavel and J. Hatcliff, Eds. Lecture Notes in Computer Science","volume":"2619","author":"Conchon S.","unstructured":"Conchon , S. and Krsti\u0107 , S . 2003. Strategies for combining decision procedures . In Proceedings of the International Conference on Tools and Algorithms for Constitution and Analysis of Systems, H. Garavel and J. Hatcliff, Eds. Lecture Notes in Computer Science , vol. 2619 . Springer-Verlag, Berlin, Germany, 537--553. Conchon, S. and Krsti\u0107, S. 2003. Strategies for combining decision procedures. In Proceedings of the International Conference on Tools and Algorithms for Constitution and Analysis of Systems, H. Garavel and J. Hatcliff, Eds. Lecture Notes in Computer Science, vol. 2619. Springer-Verlag, Berlin, Germany, 537--553."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 13th International Conference on Automated Deduction, M. A. McRobbie and J. K. Slaney, Eds. Lecture Notes in Artificial Intelligence","volume":"1104","author":"Cyrluk D.","unstructured":"Cyrluk , D. , Lincoln , P. , and Shankar , N . 1996. On Shostak's decision procedure for combination of theories . In Proceedings of the 13th International Conference on Automated Deduction, M. A. McRobbie and J. K. Slaney, Eds. Lecture Notes in Artificial Intelligence , vol. 1104 . Springer-Verlag, Berlin, Germany, 463--477. Cyrluk, D., Lincoln, P., and Shankar, N. 1996. On Shostak's decision procedure for combination of theories. In Proceedings of the 13th International Conference on Automated Deduction, M. A. McRobbie and J. K. Slaney, Eds. Lecture Notes in Artificial Intelligence, vol. 1104. Springer-Verlag, Berlin, Germany, 463--477."},{"key":"e_1_2_1_26_1","volume-title":"Tech. Rep. UIB96-08, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Ulm","author":"Cyrluk D.","year":"1996","unstructured":"Cyrluk , D. , M\u00f6ller , O. , and Ruess , H . 1996 . An efficient decision procedure for a theory of fixed-sized bitvectors with composition and extraction. Tech. Rep. UIB96-08, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Ulm , Ulm, Germany . Cyrluk, D., M\u00f6ller, O., and Ruess, H. 1996. An efficient decision procedure for a theory of fixed-sized bitvectors with composition and extraction. Tech. Rep. UIB96-08, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Ulm, Ulm, Germany."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 2nd International Joint Conference on Automated Reasoning, D. Basin and M. Rusinowitch, Eds. Lecture Notes in Artificial Intelligence","volume":"3097","author":"de Moura L.","unstructured":"de Moura , L. , Owre , S. , Ruess , H. , Rushby , J. , and Shankar , N . 2004. The ICS decision procedures for embedded deduction . In Proceedings of the 2nd International Joint Conference on Automated Reasoning, D. Basin and M. Rusinowitch, Eds. Lecture Notes in Artificial Intelligence , vol. 3097 . Springer-Verlag, Berlin, Germany, 218--222. de Moura, L., Owre, S., Ruess, H., Rushby, J., and Shankar, N. 2004. The ICS decision procedures for embedded deduction. In Proceedings of the 2nd International Joint Conference on Automated Reasoning, D. Basin and M. Rusinowitch, Eds. Lecture Notes in Artificial Intelligence, vol. 3097. Springer-Verlag, Berlin, Germany, 218--222."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 18th International Conference on Automated Deduction, A. Voronkov, Ed. Lecture Notes in Artificial Intelligence","volume":"2392","author":"de Moura L.","unstructured":"de Moura , L. , Ruess , H. , and Sorea , M . 2002. Lazy theorem proving for bounded model checking over infinite domains . In Proceedings of the 18th International Conference on Automated Deduction, A. Voronkov, Ed. Lecture Notes in Artificial Intelligence , vol. 2392 . Springer-Verlag, Berlin, Germany, 438--455. de Moura, L., Ruess, H., and Sorea, M. 2002. Lazy theorem proving for bounded model checking over infinite domains. In Proceedings of the 18th International Conference on Automated Deduction, A. Voronkov, Ed. Lecture Notes in Artificial Intelligence, vol. 2392. Springer-Verlag, Berlin, Germany, 438--455."},{"volume-title":"Proceedings SEFM03","author":"D\u00e9harbe D.","key":"e_1_2_1_29_1","unstructured":"D\u00e9harbe , D. and Ranise , S . 2003. Light-weight theorem proving for debugging and verifying units of code . In Proceedings SEFM03 . IEEE Computer Society Press, Los Alamitos, CA. D\u00e9harbe, D. and Ranise, S. 2003. Light-weight theorem proving for debugging and verifying units of code. In Proceedings SEFM03. IEEE Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/648338.755908"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Dershowitz N. and Plaisted D. A. 2001. Rewriting. In Handbook of Automated Reasoning A. Robinson and A. Voronkov Eds. Vol. 1. Elsevier Amsterdam The Netherlands 535--610.  Dershowitz N. and Plaisted D. A. 2001. Rewriting. In Handbook of Automated Reasoning A. Robinson and A. Voronkov Eds. Vol. 1. Elsevier Amsterdam The Netherlands 535--610.","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512777"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Verification","author":"Dutertre B.","key":"e_1_2_1_35_1","unstructured":"Dutertre , B. and de Moura , L. 2006. A fast linear-arithmetic solver for DPLL(T) . In Proceedings of the International Conference on Computer-Aided Verification , T. Ball and R. B. Jones, Eds. Lecture Notes in Computer Science, vol. 4144 . Springer-Verlag , Berlin, Germany, 81--94. Dutertre, B. and de Moura, L. 2006. A fast linear-arithmetic solver for DPLL(T). In Proceedings of the International Conference on Computer-Aided Verification, T. Ball and R. B. Jones, Eds. Lecture Notes in Computer Science, vol. 4144. Springer-Verlag, Berlin, Germany, 81--94."},{"key":"e_1_2_1_36_1","first-page":"1793","article-title":"Resolution decision procedures. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier, Amsterdam, The Netherlands","volume":"25","author":"Ferm\u00fcller C.","year":"2001","unstructured":"Ferm\u00fcller , C. , Leitsch , A. , Hustadt , U. , and Tammet , T. 2001 . Resolution decision procedures. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier, Amsterdam, The Netherlands , Chapter 25 , 1793 -- 1849 . Ferm\u00fcller, C., Leitsch, A., Hustadt, U., and Tammet, T. 2001. Resolution decision procedures. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier, Amsterdam, The Netherlands, Chapter 25, 1793--1849.","journal-title":"Chapter"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification, J. Warren, W. A. Hunt, Jr., and F. Somenzi, Eds. Lecture Notes in Computer Science","volume":"2725","author":"Flanagan C.","unstructured":"Flanagan , C. , Joshi , R. , Ou , X. , and Saxe , J. B . 2003. Theorem proving using lazy proof explication . In Proceedings of the International Conference on Computer-Aided Verification, J. Warren, W. A. Hunt, Jr., and F. Somenzi, Eds. Lecture Notes in Computer Science , vol. 2725 . Springer-Verlag, Berlin, Germany, 355--367. Flanagan, C., Joshi, R., Ou, X., and Saxe, J. B. 2003. Theorem proving using lazy proof explication. In Proceedings of the International Conference on Computer-Aided Verification, J. Warren, W. A. Hunt, Jr., and F. Somenzi, Eds. Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, Berlin, Germany, 355--367."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138032"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/648238.761388"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 16th International Conference on Computer-Aided Verification (CAV'04)","volume":"3114","author":"Ganzinger H.","unstructured":"Ganzinger , H. , Hagen , G. , Nieuwenhuis , R. , Oliveras , A. , and Tinelli , C . 2004a. DPLL(T): Fast decision procedures . In Proceedings of the 16th International Conference on Computer-Aided Verification (CAV'04) , R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science , vol. 3114 . Springer-Verlag, Berlin, Germany, 175--188. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., and Tinelli, C. 2004a. DPLL(T): Fast decision procedures. In Proceedings of the 16th International Conference on Computer-Aided Verification (CAV'04), R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 175--188."},{"key":"e_1_2_1_41_1","volume-title":"Tech. Rep. CSL-SRI-04-02, SRI International","author":"Ganzinger H.","year":"2004","unstructured":"Ganzinger , H. , Ruess , H. , and Shankar , N . 2004 b. Modularity and refinement in inference systems. Tech. Rep. CSL-SRI-04-02, SRI International , Menlo Park, CA . Ganzinger, H., Ruess, H., and Shankar, N. 2004b. Modularity and refinement in inference systems. Tech. Rep. CSL-SRI-04-02, SRI International, Menlo Park, CA."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.10.002"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the 5th International Worshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence","volume":"3717","author":"Ghilardi S.","unstructured":"Ghilardi , S. , Nicolini , E. , and Zucchelli , D . 2005. A comprehensive framework for combined decision procedures . In Proceedings of the 5th International Worshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence , vol. 3717 . Springer-Verlag, Berlin, Germany, 1--30. Ghilardi, S., Nicolini, E., and Zucchelli, D. 2005. A comprehensive framework for combined decision procedures. In Proceedings of the 5th International Worshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 1--30."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268661"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_2_1_47_1","volume-title":"Eds","author":"Kaufmann M.","year":"2000","unstructured":"Kaufmann , M. , Manolios , P. , and Moore , J. S . Eds . 2000 . Computer Aided Reasoning: ACL2 Case Studies . Kluwer . Kaufmann, M., Manolios, P., and Moore, J. S. Eds. 2000. Computer Aided Reasoning: ACL2 Case Studies. Kluwer."},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of 2nd ICTAC, D. Hung and M. Wirsing, Eds. Lecture Notes in Computer Science","volume":"3722","author":"Kirchner H.","unstructured":"Kirchner , H. , Ranise , S. , Ringeissen , C. , and Tran , D. K . 2005. On superposition-based satisfiability procedures and their combination . In Proceedings of 2nd ICTAC, D. Hung and M. Wirsing, Eds. Lecture Notes in Computer Science , vol. 3722 . Springer-Verlag, Berlin, Germany, 594--608. Kirchner, H., Ranise, S., Ringeissen, C., and Tran, D. K. 2005. On superposition-based satisfiability procedures and their combination. In Proceedings of 2nd ICTAC, D. Hung and M. Wirsing, Eds. Lecture Notes in Computer Science, vol. 3722. Springer-Verlag, Berlin, Germany, 594--608."},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Knuth D. E. and Bendix P. B. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra J. Leech Ed. Pergamon Press Oxford UK 263--297.  Knuth D. E. and Bendix P. B. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra J. Leech Ed. Pergamon Press Oxford UK 263--297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"e_1_2_1_50_1","volume-title":"Proc. CADE-19","volume":"2741","author":"Krsti\u0107 S.","unstructured":"Krsti\u0107 , S. and Conchon , S . 2003. Canonization for disjoint unions of theories . In Proc. CADE-19 , F. Baader, Ed. Lecture Notes in Computer Science , vol. 2741 . Springer-Verlag, Berlin, Germany. Krsti\u0107, S. and Conchon, S. 2003. Canonization for disjoint unions of theories. In Proc. CADE-19, F. Baader, Ed. Lecture Notes in Computer Science, vol. 2741. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 5th FroCoS, B. Gramlich, Ed. Lecture Notes in Artificial Intelligence","volume":"3717","author":"Lahiri S. K.","unstructured":"Lahiri , S. K. and Musuvathi , M . 2005a. An efficient decision procedure for UTVPI constraints . In Proceedings of the 5th FroCoS, B. Gramlich, Ed. Lecture Notes in Artificial Intelligence , vol. 3717 . Springer-Verlag, Berlin, Germany, 168--183. Lahiri, S. K. and Musuvathi, M. 2005a. An efficient decision procedure for UTVPI constraints. In Proceedings of the 5th FroCoS, B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 168--183."},{"volume-title":"Notes 3rd PDPAR Workshop, CAV-17","author":"Lahiri S. K.","key":"e_1_2_1_52_1","unstructured":"Lahiri , S. K. and Musuvathi , M . 2005b. An efficient Nelson-Oppen decision procedure for difference constraints over rationals . In Notes 3rd PDPAR Workshop, CAV-17 . 2--9. Lahiri, S. K. and Musuvathi, M. 2005b. An efficient Nelson-Oppen decision procedure for difference constraints over rationals. In Notes 3rd PDPAR Workshop, CAV-17. 2--9."},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of CAV-16","volume":"3114","author":"Lahiri S. K.","unstructured":"Lahiri , S. K. and Seshia , S. A . 2004. The UCLID decision procedure . In Proceedings of CAV-16 , R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science , vol. 3114 . Springer-Verlag, Berlin, Germany, 475--478. Lahiri, S. K. and Seshia, S. A. 2004. The UCLID decision procedure. In Proceedings of CAV-16, R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 475--478."},{"volume-title":"Automatic Theorem Proving Project","author":"Lankford D. S.","key":"e_1_2_1_54_1","unstructured":"Lankford , D. S. 1975. Canonical inference. Memo ATP-32 , Automatic Theorem Proving Project , University of Texas , Austin, TX . Lankford, D. S. 1975. Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX."},{"volume-title":"Proceedings of LICS-17","author":"Lynch C.","key":"e_1_2_1_55_1","unstructured":"Lynch , C. and Morawska , B . 2002. Automatic decidability . In Proceedings of LICS-17 , G. Plotkin, Ed. IEEE Computer Society Press, Los Alamitos, CA. Lynch, C. and Morawska, B. 2002. Automatic decidability. In Proceedings of LICS-17, G. Plotkin, Ed. IEEE Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_22"},{"key":"e_1_2_1_57_1","series-title":"Lecture Notes in Computer Science","volume-title":"Crossroads: From Panacea to Foundational Support","author":"Manna Z.","year":"2003","unstructured":"Manna , Z. and Zarba , C. G . 2003 . Combining decision procedures. In Formal Methods at the Crossroads: From Panacea to Foundational Support . Lecture Notes in Computer Science , vol. 2757 . Springer-Verlag , Berlin, Germany, 381--422. Manna, Z. and Zarba, C. G. 2003. Combining decision procedures. In Formal Methods at the Crossroads: From Panacea to Foundational Support. Lecture Notes in Computer Science, vol. 2757. Springer-Verlag, Berlin, Germany, 381--422."},{"volume-title":"Argonne National Laboratory","author":"McCune W. W.","key":"e_1_2_1_58_1","unstructured":"McCune , W. W. 2003. Otter 3.3 reference manual. Tech. Rep. ANL\/MCS-TM-263, MCS Division , Argonne National Laboratory , Argonne, IL, U.S.A. McCune, W. W. 2003. Otter 3.3 reference manual. Tech. Rep. ANL\/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne, IL, U.S.A."},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the CAV-17","volume":"3576","author":"Meir O.","unstructured":"Meir , O. and Strichman , O . 2005. Yet another decision procedure for equality logic . In Proceedings of the CAV-17 , K. Etessami and S. Rajamani, Eds. Lecture Notes in Computer Science , vol. 3576 . Springer-Verlag, Berlin, Germany, 307--320. Meir, O. and Strichman, O. 2005. Yet another decision procedure for equality logic. In Proceedings of the CAV-17, K. Etessami and S. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, Berlin, Germany, 307--320."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"volume-title":"Proceedings of the LICS-13","author":"Necula G.","key":"e_1_2_1_61_1","unstructured":"Necula , G. and Lee , P . 1998. Efficient representation and validation of proofs . In Proceedings of the LICS-13 , V. Pratt, Ed. IEEE Computer Society Press, Los Alamitos, CA, 93--104. Necula, G. and Lee, P. 1998. Efficient representation and validation of proofs. In Proceedings of the LICS-13, V. Pratt, Ed. IEEE Computer Society Press, Los Alamitos, CA, 93--104."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.009"},{"key":"e_1_2_1_65_1","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis R. and Rubio A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning A. Robinson and A. Voronkov Eds. Vol. 1. Elsevier Amsterdam The Netherlands 371--443.  Nieuwenhuis R. and Rubio A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning A. Robinson and A. Voronkov Eds. Vol. 1. Elsevier Amsterdam The Netherlands 371--443.","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/322203.322204"},{"key":"e_1_2_1_67_1","volume-title":"PVS: A prototype verification system. In Proceedings of the International Conference on Automated Dedication","author":"Owre S.","year":"1992","unstructured":"Owre , S. , Rushby , J. M. , and Shankar , N . 1992 . PVS: A prototype verification system. In Proceedings of the International Conference on Automated Dedication , D. Kapur, Ed. Lecture Notes in Artificial Intelligence, vol. 607 . Springer-Verlag , Berlin, Germany, 748--752. Owre, S., Rushby, J. M., and Shankar, N. 1992. PVS: A prototype verification system. In Proceedings of the International Conference on Automated Dedication, D. Kapur, Ed. Lecture Notes in Artificial Intelligence, vol. 607. Springer-Verlag, Berlin, Germany, 748--752."},{"key":"e_1_2_1_68_1","series-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","volume-title":"Logical Foundations","author":"Plaisted D. A.","unstructured":"Plaisted , D. A. 1993. Equational reasoning and term rewriting systems . In Handbook of Logic in Artificial Intelligence and Logic Programming , D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Eds. Vol. I : Logical Foundations . Oxford University Press , Oxford, UK , 273--364. Plaisted, D. A. 1993. Equational reasoning and term rewriting systems. In Handbook of Logic in Artificial Intelligence and Logic Programming, D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Eds. Vol. I: Logical Foundations. Oxford University Press, Oxford, UK, 273--364."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0028"},{"volume-title":"Proceedings of FTP-2003","author":"Ranise S.","key":"e_1_2_1_70_1","unstructured":"Ranise , S. and D\u00e9harbe , D . 2003. Light-weight theorem proving for debugging and verifying pointer manipulating programs . In Proceedings of FTP-2003 , I. Dahn and L. Vigneron, Eds. Number DSCI--II710\/03 in Technical Reports. Universidad Polit\u00e9cnica de Valencia, 119--132. Ranise, S. and D\u00e9harbe, D. 2003. Light-weight theorem proving for debugging and verifying pointer manipulating programs. In Proceedings of FTP-2003, I. Dahn and L. Vigneron, Eds. Number DSCI--II710\/03 in Technical Reports. Universidad Polit\u00e9cnica de Valencia, 119--132."},{"volume-title":"Proceedings of the 1st ICTAC, K. Araki and Z. Liu, Eds. Lecture Notes in Computer Science. Springer-Verlag","author":"Ranise S.","key":"e_1_2_1_71_1","unstructured":"Ranise , S. , Ringeissen , C. , and Tran , D. K . 2004. Nelson-Oppen, Shostak and the extended canonizer: A family picture with a newborn . In Proceedings of the 1st ICTAC, K. Araki and Z. Liu, Eds. Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany. Ranise, S., Ringeissen, C., and Tran, D. K. 2004. Nelson-Oppen, Shostak and the extended canonizer: A family picture with a newborn. In Proceedings of the 1st ICTAC, K. Araki and Z. Liu, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_72_1","volume-title":"Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence","volume":"3717","author":"Ranise S.","unstructured":"Ranise , S. , Ringeissen , C. , and Zarba , C. G . 2005. Combining data structures with nonstably infinite theories using many-sorted logic . In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence , vol. 3717 . Springer-Verlag, Berlin, Germany, 48--64. Ranise, S., Ringeissen, C., and Zarba, C. G. 2005. Combining data structures with nonstably infinite theories using many-sorted logic. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 48--64."},{"key":"e_1_2_1_73_1","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov A.","year":"2002","unstructured":"Riazanov , A. and Voronkov , A. 2002 . The design and implementation of VAMPIRE . J. AI Commun. 15 , 2\/3, 91--110. Riazanov, A. and Voronkov, A. 2002. The design and implementation of VAMPIRE. J. AI Commun. 15, 2\/3, 91--110.","journal-title":"J. AI Commun."},{"key":"e_1_2_1_74_1","unstructured":"Ruess H. 2004. Personal communication on ICS 2.0 (e-mail message to Alessandro Armando).  Ruess H. 2004. Personal communication on ICS 2.0 (e-mail message to Alessandro Armando)."},{"volume-title":"Deconstructing Shostak. In Proceedings of the IEEE Symposium on Logic in Computer Science. J. Halpern, Ed. IEEE Computer Society Press","author":"Ruess H.","key":"e_1_2_1_75_1","unstructured":"Ruess , H. and Shankar , N . 2001 . Deconstructing Shostak. In Proceedings of the IEEE Symposium on Logic in Computer Science. J. Halpern, Ed. IEEE Computer Society Press , Los Alamitos, CA. Ruess, H. and Shankar, N. 2001. Deconstructing Shostak. In Proceedings of the IEEE Symposium on Logic in Computer Science. J. Halpern, Ed. IEEE Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_76_1","volume-title":"Tech. Rep. CSL-SRI-04-01, SRI International","author":"Ruess H.","year":"2004","unstructured":"Ruess , H. and Shankar , N . 2004 . Solving linear arithmetic constraints. Tech. Rep. CSL-SRI-04-01, SRI International , Menlo Park, CA . Ruess, H. and Shankar, N. 2004. Solving linear arithmetic constraints. Tech. Rep. CSL-SRI-04-01, SRI International, Menlo Park, CA."},{"key":"e_1_2_1_77_1","first-page":"2","article-title":"E\u2014A brainiac theorem prover","volume":"15","author":"Schulz S.","year":"2002","unstructured":"Schulz , S. 2002 . E\u2014A brainiac theorem prover . J. AI Commun. 15 , 2 -- 3 , 111--126. Schulz, S. 2002. E\u2014A brainiac theorem prover. J. AI Commun. 15, 2--3, 111--126.","journal-title":"J. AI Commun."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25984-8_15"},{"volume-title":"Notes 5th IWIL Workshop, LPAR-11","author":"Schulz S.","key":"e_1_2_1_79_1","unstructured":"Schulz , S. and Bonacina , M. P . 2005. On handling distinct objects in the superposition calculus . In Notes 5th IWIL Workshop, LPAR-11 . 66--77. Schulz, S. and Bonacina, M. P. 2005. On handling distinct objects in the superposition calculus. In Notes 5th IWIL Workshop, LPAR-11. 66--77."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775945"},{"key":"e_1_2_1_81_1","volume-title":"Little engines of proof. Invited talk","author":"Shankar N.","year":"2003","unstructured":"Shankar , N. 2002. Little engines of proof. Invited talk , 3rd FLoC, Copenhagen , Denmark; and course notes of Fall 2003 , http:\/\/www.csl.sri.com\/users\/shankar\/LEP.html. Shankar, N. 2002. Little engines of proof. Invited talk, 3rd FLoC, Copenhagen, Denmark; and course notes of Fall 2003, http:\/\/www.csl.sri.com\/users\/shankar\/LEP.html."},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359570"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"volume-title":"Herbrand Award speech","author":"Stickel M. E.","key":"e_1_2_1_84_1","unstructured":"Stickel , M. E. 2002. Herbrand Award speech . 3rd FLoC, Copenhagen, Denmark . Stickel, M. E. 2002. Herbrand Award speech. 3rd FLoC, Copenhagen, Denmark."},{"key":"e_1_2_1_85_1","unstructured":"Stump A. 2005. Personal communication on CVC 1.0a (e-mail message to Alessandro Armando).  Stump A. 2005. Personal communication on CVC 1.0a (e-mail message to Alessandro Armando)."},{"key":"e_1_2_1_86_1","volume-title":"CVC: A Cooperating Validity Checker. In Proc. CAV-14","author":"Stump A.","year":"2002","unstructured":"Stump , A. , Barrett , C. W. , and Dill , D. L . 2002 . CVC: A Cooperating Validity Checker. In Proc. CAV-14 , K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science, vol. 2404 . Springer-Verlag , Berlin, Germany, 500--504. Stump, A., Barrett, C. W., and Dill, D. L. 2002. CVC: A Cooperating Validity Checker. In Proc. CAV-14, K. G. Larsen and E. Brinksma, Eds. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany, 500--504."},{"volume-title":"Proceedings of LICS-16","author":"Stump A.","key":"e_1_2_1_87_1","unstructured":"Stump , A. , Barrett , C. W. , Dill , D. L. , and Levitt , J . 2001. A decision procedure for an extensional theory of arrays . In Proceedings of LICS-16 , J. Halpern, Ed. IEEE Computer Society Press, Los Alamitos, CA. Stump, A., Barrett, C. W., Dill, D. L., and Levitt, J. 2001. A decision procedure for an extensional theory of arrays. In Proceedings of LICS-16, J. Halpern, Ed. IEEE Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_88_1","volume-title":"Proceedings of CADE-18","volume":"2392","author":"Stump A.","unstructured":"Stump , A. and Dill , D. L . 2002. Faster proof checking in the Edinburgh Logical Framework . In Proceedings of CADE-18 , A. Voronkov, Ed. Lecture Notes in Artificial Intelligence , vol. 2392 . Springer-Verlag, Berlin, Germany, 392--407. Stump, A. and Dill, D. L. 2002. Faster proof checking in the Edinburgh Logical Framework. In Proceedings of CADE-18, A. Voronkov, Ed. Lecture Notes in Artificial Intelligence, vol. 2392. Springer-Verlag, Berlin, Germany, 392--407."},{"key":"e_1_2_1_89_1","volume-title":"Proceedings of the 1st FroCoS, F. Baader and K. Schulz, Eds. Applied Logic Series","volume":"3","author":"Tinelli C.","unstructured":"Tinelli , C. and Harandi , M . 1996. A new correctness proof of the Nelson-Oppen combination procedure . In Proceedings of the 1st FroCoS, F. Baader and K. Schulz, Eds. Applied Logic Series , vol. 3 . Kluwer Academic Publishers. Tinelli, C. and Harandi, M. 1996. A new correctness proof of the Nelson-Oppen combination procedure. In Proceedings of the 1st FroCoS, F. Baader and K. Schulz, Eds. Applied Logic Series, vol. 3. Kluwer Academic Publishers."},{"volume-title":"Logic and Structure","author":"van Dalen D.","key":"e_1_2_1_90_1","unstructured":"van Dalen , D. 1989. Logic and Structure . Springer-Verlag , Berlin, Germany . Second edition. van Dalen, D. 1989. Logic and Structure. Springer-Verlag, Berlin, Germany. Second edition."},{"key":"e_1_2_1_91_1","volume-title":"Proceedings of the 16th International Conference on Automated Dedication. H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence","volume":"1632","author":"Weidenbach C.","unstructured":"Weidenbach , C. , Afshordel , B. , Brahm , U. , Cohrs , C. , Engel , T. , Keen , E. , Theobalt , C. , and Topi\u0107 , D . 1999. System description: Spass version 1.0.0 . In Proceedings of the 16th International Conference on Automated Dedication. H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence , vol. 1632 . Springer-Verlag, Berlin, Germany, 378--382. Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., and Topi\u0107, D. 1999. System description: Spass version 1.0.0. In Proceedings of the 16th International Conference on Automated Dedication. H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, Berlin, Germany, 378--382."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1459010.1459014","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1459010.1459014","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:58Z","timestamp":1750253398000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1459010.1459014"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":91,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1145\/1459010.1459014"],"URL":"https:\/\/doi.org\/10.1145\/1459010.1459014","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2009,1]]},"assertion":[{"value":"2006-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}