Narrowing and Rewriting Logic: from Foundations to Applications

Santiago Escobar, José Meseguer, Prasanna Thati

Research output: Contribution to journalArticle

Abstract

Narrowing was originally introduced to solve equational E-unification problems. It has also been recognized as a key mechanism to unify functional and logic programming. In both cases, narrowing supports equational reasoning and assumes confluent equations. The main goal of this work is to show that narrowing can be greatly generalized, so as to support a much wider range of applications, when it is performed with rewrite theories (Σ, E, R), where (Σ, E) is an equational theory, and R is a collection of rewrite rules with no restrictions. Such theories axiomatize concurrent systems, whose states are equivalence classes of terms modulo E, and whose transitions are specified by R. In this context, narrowing is generalized from an equational reasoning technique to a symbolic model checking technique for reachability analysis of a, typically infinite, concurrent system. We survey the foundations of this approach, suitable narrowing strategies, and various applications to security protocol verification, theorem proving, and programming languages.

Original languageEnglish (US)
Pages (from-to)5-33
Number of pages29
JournalElectronic Notes in Theoretical Computer Science
Volume177
Issue number1
DOIs
StatePublished - Jun 1 2007

Keywords

  • Equational Reasoning
  • Maude
  • Narrowing
  • Reachability
  • Rewriting Logic
  • Security protocols

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Narrowing and Rewriting Logic: from Foundations to Applications'. Together they form a unique fingerprint.

  • Cite this