Equational and Inductive Reasoning for Maude in Athena

TL;DR

This paper introduces maude2athena, a translation framework that enables inductive and equational reasoning over Maude specifications within Athena, bridging model checking and theorem proving.

Contribution

It provides a systematic translation from Maude's equational theories to Athena, supporting inductive proofs modulo structural axioms with a compact and semantics-preserving encoding.

Findings

Supports induction-based reasoning modulo structural axioms

Faithfully encodes membership equational logic in a many-sorted setting

Maintains semantics and compactness of the original specifications

Abstract

In the rewriting logic framework, equational-based specifications are used to define deterministic functional behavior, abstract data types, and canonical representations of data. These specifications include a (possibly order-sorted) signature and equations interpreted modulo structural axioms, such as associativity, commutativity, and identity. While equational rewriting provides a powerful basis for execution and symbolic reasoning, it does not by itself offer native support for inductive or deductive reasoning. This paper presents maude2athena, a framework that systematically translates Maude's equational theories into Athena, a theorem proving language designed to support natural deduction proofs over many-sorted first-order logic specifications, including inductive reasoning, equational chaining, case-based reasoning, and proofs by contradiction. The translation supports induction-based reasoning modulo structural axioms with parametric induction rules; it faithfully encodes membership equational logic in a many-sorted setting without exponential blowup under reasonable conditions. This approach preserves the semantics of the original specification, while ensuring that the translation remains compact and amenable to deductive reasoning. This work helps bridge the gap between model checking and theorem proving, enabling formal verification efforts that can benefit from both of these approaches.