TY - CHAP
T1 - Generalized rewrite theories
AU - Bruni, Roberto
AU - Meseguer, José
PY - 2003
Y1 - 2003
N2 - Since its introduction, more than a decade ago, rewriting logic has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. In particular, the Maude system now supports subsorting and conditions in the equational logic for data, and also frozen arguments to block undesired nested rewritings; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories.
AB - Since its introduction, more than a decade ago, rewriting logic has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. In particular, the Maude system now supports subsorting and conditions in the equational logic for data, and also frozen arguments to block undesired nested rewritings; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories.
UR - http://www.scopus.com/inward/record.url?scp=35248887958&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35248887958&partnerID=8YFLogxK
U2 - 10.1007/3-540-45061-0_22
DO - 10.1007/3-540-45061-0_22
M3 - Chapter
AN - SCOPUS:35248887958
SN - 3540404937
SN - 9783540404934
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 252
EP - 266
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Baeten, Jos C. M.
A2 - Lenstra, Jan Karel
A2 - Parrow, Joachim
A2 - Woeginger, Gerhard J.
PB - Springer
ER -