{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:50:29Z","timestamp":1762458629741},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540789123"},{"type":"electronic","value":"9783540789130"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78913-0_25","type":"book-chapter","created":{"date-parts":[[2008,4,11]],"date-time":"2008-04-11T12:13:06Z","timestamp":1207915986000},"page":"337-351","source":"Crossref","is-referenced-by-count":4,"title":["Theorem Proving Modulo Based on Boolean Equational Procedures"],"prefix":"10.1007","author":[{"given":"Camilo","family":"Rocha","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","volume-title":"Program Construction: Calculating Implementations from Specifications","author":"R. Backhouse","year":"2003","unstructured":"Backhouse, R.: Program Construction: Calculating Implementations from Specifications. Willey, Chichester, UK (2003)"},{"issue":"3","key":"25_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H.P. Barendregt","year":"2002","unstructured":"Barendregt, H.P., Barendsen, E.: Autarkic computations and formal proofs. Journal of Automated Reasoning\u00a028(3), 321\u2013336 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"25_CR4","unstructured":"de Recherche en, L.: Informatique. The CiME System (2007), http:\/\/cime.lri.fr\/"},{"key":"25_CR5","series-title":"Formal Methods and Semantics, ch.\u00a06","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, ch.\u00a06, vol.\u00a0B, pp. 243\u2013320. North-Holland, Amsterdam (1990)"},{"key":"25_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)"},{"issue":"1","key":"25_CR7","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning\u00a031(1), 33\u201372 (2003)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR8","first-page":"417","volume-title":"Proc. Strategies 2006, ENTCS","author":"S. Eker","year":"2007","unstructured":"Eker, S., Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: Deduction, strategies, and rewriting. In: Mart\u00ed-Oliet, N. (ed.) Proc. Strategies 2006, ENTCS, pp. 417\u2013441. Elsevier, Amsterdam (2007)"},{"key":"25_CR9","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol.\u00a07. Cambridge University Press, Cambridge (1989)"},{"key":"25_CR10","unstructured":"Gries, D.: A calculational proof of Andrews\u2019s challenge. Technical Report TR96-1602, Cornell University, Computer Science (August 28, 1996)"},{"key":"25_CR11","volume-title":"Texts and Monographs in Computer Science","author":"D. Gries","year":"1993","unstructured":"Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. In: Texts and Monographs in Computer Science, Springer, Heidelberg (1993)"},{"issue":"3","key":"25_CR12","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/0020-0190(94)00198-8","volume":"53","author":"D. Gries","year":"1995","unstructured":"Gries, D., Schneider, F.B.: Equational propositional logic. Inf. Process. Lett.\u00a053(3), 145\u2013152 (1995)","journal-title":"Inf. Process. Lett."},{"key":"25_CR13","unstructured":"Hendrix, J., Ohsaki, H., Meseguer, J.: Sufficient completeness checking with propositional tree automata. Technical Report UIUCDCS-R-2005-2635, University of Illinois Urbana-Champaign (2005)"},{"key":"25_CR14","unstructured":"Hsiang, J.: Topics in automated theorem proving and program generation. PhD thesis, University of Illinois at Urbana-Champaign (1982)"},{"key":"25_CR15","volume-title":"Basic algebra","author":"N. Jacobson","year":"1974","unstructured":"Jacobson, N.: Basic algebra, vol.\u00a0I. W. H. Freeman and Co., San Francisco, Calif (1974)"},{"issue":"1-3","key":"25_CR16","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0168-0072(01)00059-8","volume":"113","author":"V. Lifschitz","year":"2001","unstructured":"Lifschitz, V.: On calculational proofs. Ann. Pure Appl. Logic\u00a0113(1-3), 207\u2013224 (2001)","journal-title":"Ann. Pure Appl. Logic"},{"key":"25_CR17","volume-title":"Aristotle\u2019s Syllogistic, From the Standpoint of Modern Formal Logic","author":"J. \u0141ukasiewicz","year":"1951","unstructured":"\u0141ukasiewicz, J.: Aristotle\u2019s Syllogistic, From the Standpoint of Modern Formal Logic. Oxford University Press, Oxford (1951)"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd. edn., pp. 1\u201387. Kluwer Academic Publishers, 2002. First published as SRI Tech. Report SRI-CSL-93-05 (August 1993)","DOI":"10.1007\/978-94-017-0464-9_1"},{"issue":"1\u20132","key":"25_CR19","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation\u00a020(1\u20132), 123\u2013160 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"25_CR20","unstructured":"Moss, L.S.: Syllogistic logic with complements (Draft 2007)"},{"key":"25_CR21","unstructured":"Rocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical Report 2007-2818, University of Illinois at Urbana-Champaign (2007)"},{"key":"25_CR22","unstructured":"Rocha, C., Meseguer, J.: A rewriting decision procedure for Dijkstra-Scholten\u2019s syllogistic logic with complements. Revista Colombiana de Computaci\u00f3n\u00a08(2) (2007)"},{"key":"25_CR23","unstructured":"Rocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. Technical Report 2007-2922, University of Illinois at Urbana-Champaign (2007)"},{"key":"25_CR24","volume-title":"Introduction to topology and modern analysis","author":"G.F. Simmons","year":"1963","unstructured":"Simmons, G.F.: Introduction to topology and modern analysis. McGraw-Hill Book Co., Inc, New York (1963)"},{"key":"25_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2266-8","volume-title":"Deduction Systems","author":"R. Socher-Ambrosius","year":"1997","unstructured":"Socher-Ambrosius, R., Johann, P.: Deduction Systems. Springer, Berlin (1997)"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-540-39993-3_16","volume-title":"From Object-Orientation to Formal Methods","author":"M.-O. Stehr","year":"2004","unstructured":"Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol.\u00a02635, pp. 334\u2013375. Springer, Heidelberg (2004)"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Viry, P.: Adventures in sequent calculus modulo equations. Electr. Notes Theor. Comput. Sci.\u00a015 (1998)","DOI":"10.1016\/S1571-0661(05)82550-2"},{"key":"25_CR28","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science\u00a0285, 487\u2013517 (2002)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Relations and Kleene Algebra in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78913-0_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:03:41Z","timestamp":1619521421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78913-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540789123","9783540789130"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78913-0_25","relation":{},"subject":[]}}