Symbolic reasoning methods in rewriting logic and maude

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationLogic, Language, Information, and Computation - 25th International Workshop, WoLLIC 2018, Proceedings
EditorsRuy de Queiroz, Maricarmen Martinez, Lawrence S. Moss
Number of pages36
ISBN (Print)9783662576687
StatePublished - 2018
Externally publishedYes
Event25th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2018 - Bogota, Colombia
Duration: Jul 24 2018Jul 27 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10944 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other25th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2018


  • Maude
  • Rewriting logic
  • Symbolic computation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Symbolic reasoning methods in rewriting logic and maude'. Together they form a unique fingerprint.

Cite this