TY - GEN
T1 - Symbolic reasoning methods in rewriting logic and maude
AU - Meseguer, José
N1 - Funding Information:
I thank the organizers of WoLLIC for kindly giving me the opportunity of presenting these ideas in Bogotá. As the references make clear, these ideas have been developed in joint work with a large number of collaborators and former or present students, and in dialogue with many other colleagues. I cannot mention them all and apologize in advance for this; but I would like to mention and cordially thank in particular: María Alpuente, Kyungmin Bae, Andrew Cholewa, Angel CuencaOrtega, Francisco Durán, Steven Eker, Santiago Escobar, Raúl Gutiérrez, Joseph Hendrix, Dorel Lucanu, Salvador Lucas, Narciso Martí-Oliet, Catherine Meadows, César A. Muñoz, Hitoshi Ohsaki, Camilo Rocha, Grigore Rosu, Vlad Rusu, Sonia Santiago, Ralf Sasse, Andrei Stefanescu, Carolyn Talcott, Prasanna Thati, and Fan Yang. This work has been partially supported by NRL under contract number N00173-17-1-G002.
Publisher Copyright:
© Springer-Verlag GmbH Germany, part of Springer Nature 2018.
PY - 2018
Y1 - 2018
N2 - Rewriting logic is both a logical framework where many logics can be naturally represented, and a semantic framework where many computational systems and programming languages, including concurrent ones, can be both specified and executed. Maude is a declarative specification and programming language based on rewriting logic. For reasoning about the logics and systems represented in the rewriting logic framework symbolic methods are of great importance. This paper discusses various symbolic methods that address crucial reasoning needs in rewriting logic, how they are supported by Maude and other symbolic engines, and various applications that these methods and engines make possible. Because of the generality of rewriting logic, these methods are widely applicable: they can be used in many areas and can provide useful reasoning components for other reasoning engines.
AB - Rewriting logic is both a logical framework where many logics can be naturally represented, and a semantic framework where many computational systems and programming languages, including concurrent ones, can be both specified and executed. Maude is a declarative specification and programming language based on rewriting logic. For reasoning about the logics and systems represented in the rewriting logic framework symbolic methods are of great importance. This paper discusses various symbolic methods that address crucial reasoning needs in rewriting logic, how they are supported by Maude and other symbolic engines, and various applications that these methods and engines make possible. Because of the generality of rewriting logic, these methods are widely applicable: they can be used in many areas and can provide useful reasoning components for other reasoning engines.
KW - Maude
KW - Rewriting logic
KW - Symbolic computation
UR - http://www.scopus.com/inward/record.url?scp=85049648148&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85049648148&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-57669-4_2
DO - 10.1007/978-3-662-57669-4_2
M3 - Conference contribution
AN - SCOPUS:85049648148
SN - 9783662576687
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 25
EP - 60
BT - Logic, Language, Information, and Computation - 25th International Workshop, WoLLIC 2018, Proceedings
A2 - de Queiroz, Ruy
A2 - Martinez, Maricarmen
A2 - Moss, Lawrence S.
PB - Springer
T2 - 25th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2018
Y2 - 24 July 2018 through 27 July 2018
ER -