{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T07:40:53Z","timestamp":1725608453310},"publisher-location":"Vienna","reference-count":18,"publisher":"Springer Vienna","isbn-type":[{"type":"print","value":"9783211832820"},{"type":"electronic","value":"9783709163559"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/978-3-7091-6355-9_2","type":"book-chapter","created":{"date-parts":[[2011,9,15]],"date-time":"2011-09-15T07:42:02Z","timestamp":1316072522000},"page":"18-32","source":"Crossref","is-referenced-by-count":0,"title":["Model Elimination with Simplification and its Application to Software Verification"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Dorothea","family":"Sch\u00e4fer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Owen L. Astrachan. Investigations in Model Elimination based Theorem Proving PhD thesis, Duke University, 1992. Technical Report CS-1992\u201321."},{"key":"2_CR2","volume-title":"Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction. A Basis for Applications, volume I: Foundations. Calculi and Refinements, pages 353-398. Kluwer Academic Publishers","author":"L Bachmair","year":"1998","unstructured":"Leo Bachmair and Harald Ganzinger. Chapter 11: Equational Reasoning in Saturation-Based Theorem Proving. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction. A Basis for Applications, volume I: Foundations. Calculi and Refinements, pages 353\u2013398. Kluwer Academic Publishers, 1998."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Peter Baumgartner and Ulrich Furbach. PRO-TEIN: A PROver with a Theory Extension Interface. In A. Bundy, editor, Au-tomated Deduction - CADE-12,volume 814 of Lecture Notes in Artificial Intelligence,pages 769\u2013773. Springer, 1994. Available in the WWW, URL: http:\/\/www.uni-koblenz. de \/ag-ki\/Systems\/PROTEIN\/.","DOI":"10.1007\/3-540-58156-1_57"},{"issue":"3","key":"2_CR4","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"Bernhard Beckert and Joachim Posegga. leanT\u2019P","year":"1995","unstructured":"Bernhard Beckert and Joachim Posegga. leanT\u2019P: Lean tableau-based deduction. Journal of Automated Reasoning, 15 (3): 339\u2013358, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR5","volume-title":"Academic Press","author":"RS Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1988."},{"key":"2_CR6","first-page":"656","volume-title":"Proceedings of the Third International Workshop on Conditional Term Rewriting Systems, pages 242-256","author":"F Bronsard","year":"1992","unstructured":"Francois Bronsard and Uday S. Reddy. Reduction Techniques for First-Order Reasoning. In M. Rusinowitch and J.L. R\u00e9my, editors, Proceedings of the Third International Workshop on Conditional Term Rewriting Systems, pages 242\u2013256. Springer-Verlag, July 1992. LNCS 656."},{"issue":"6","key":"2_CR7","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1093\/jigpal\/3.6.857","volume":"3","author":"S Br\u00fcning","year":"1995","unstructured":"S. Br\u00fcning. Exploiting Equivalences in Connection Calculi. Journal of the IGPL, 3 (6): 857\u2013886, 1995.","journal-title":"Journal of the IGPL"},{"key":"2_CR8","volume-title":"Academic Press","author":"C Chang","year":"1973","unstructured":"C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"2_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1990","unstructured":"M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990."},{"key":"2_CR10","volume-title":"Cambridge University Press","author":"MJC Gordon","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"2_CR11","volume-title":"Proceedings of Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23-34 IEEE Computer Society Press","author":"M Kaufmann","year":"1996","unstructured":"M. Kaufmann and J.S. Moore. Ac12: An industrial strength version of nqthm. In Proceedings of Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23\u201334 IEEE Computer Society Press, 1996."},{"key":"2_CR12","volume-title":"Reasoning with Predicate Replacement","author":"L Shie-Jue","year":"1989","unstructured":"Shie-Jue Lee and David A. Plaisted. Reasoning with Predicate Replacement, 1989."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"D. Loveland. A Simplified Version for the Model Elimination Theorem Proving Procedure. JACM, 16 (3), 1969.","DOI":"10.1145\/321526.321527"},{"key":"2_CR14","doi-asserted-by":"publisher","DOI":"10.2172\/10129052","volume-title":"OTTER 3.0 reference manual and guide. Technical Report ANL-94\/6","author":"WW McCune","year":"1994","unstructured":"William W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94\/6, National Laboratory, Argonne, IL, 1994."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow and Lawrence C. Paulson. Isabelle-91. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction,pages 673676, Saratoga Springs, NY, 1992. Springer-Verlag LNAI 607. System abstract.","DOI":"10.1007\/3-540-55602-8_201"},{"key":"2_CR16","unstructured":"Dorothea Sch\u00e4fer. Simplification in model elimination. Master\u2019s thesis, Universit\u00e4t Koblenz, 1998. To appear."},{"key":"2_CR17","unstructured":"Gerhard Schellhorn and Wolfgang Reif. Proving properties of finite enumerations: A problem set for automated theorem provers. Technical report, University of Ulm, Dept. of Computer Science, 1997. URL: http:\/\/www.informatik.uniulm.de \/pm\/kiv\/setheo\/enum.ps."},{"key":"2_CR18","volume-title":"Sorts and Types in Artificial Intelligence, volume 418 of Lecture Notes in Artificial Intelligence, pages 49-60. Springer","author":"PH Schmitt","year":"1989","unstructured":"P.H. Schmitt and W. Wernecke. Tableau calculus for sorted logics. In Sorts and Types in Artificial Intelligence, volume 418 of Lecture Notes in Artificial Intelligence, pages 49\u201360. Springer, 1989."}],"container-title":["Tool Support for System Specification, Development and Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-7091-6355-9_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T09:36:05Z","timestamp":1606124165000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-7091-6355-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783211832820","9783709163559"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-7091-6355-9_2","relation":{},"subject":[],"published":{"date-parts":[[1999]]}}}