pith. sign in

arxiv: 2604.19475 · v1 · submitted 2026-04-21 · 💻 cs.LO

Equational and Inductive Reasoning for Maude in Athena

Mateo Sanabria , Carlos Varela , Camilo Rocha , Nicolas Cardozo This is my paper

Pith reviewed 2026-05-10 01:33 UTC · model grok-4.3

classification 💻 cs.LO
keywords MaudeAthenaequational reasoninginductive reasoningrewriting logictheorem provingmembership equational logicstructural axioms
0
0 comments X

The pith

A translation converts Maude equational theories into Athena to support inductive reasoning modulo structural axioms.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a systematic way to convert Maude equational specifications, which define functional behavior and data types using equations interpreted modulo axioms such as associativity and commutativity, into the Athena theorem-proving language. This conversion adds support for natural deduction proofs, equational chaining, case analysis, contradiction, and induction over many-sorted logic. A sympathetic reader cares because equational rewriting alone lacks native inductive reasoning, so the bridge enables verification that combines execution with deductive proofs. The translation employs parametric induction rules and encodes membership equational logic without exponential growth in theory size under typical conditions while preserving original meaning.

Core claim

The central claim is that the translation supports induction-based reasoning modulo structural axioms with parametric induction rules, faithfully encodes membership equational logic in a many-sorted setting without exponential blowup under reasonable conditions, preserves the semantics of the original Maude specification, and keeps the result compact and suitable for deductive reasoning.

What carries the argument

The translation that maps Maude order-sorted signatures and equations modulo axioms into many-sorted first-order logic with inductive capabilities.

If this is right

  • Equational specifications gain the ability to undergo both rewriting execution and inductive theorem proving in one workflow.
  • Verification can combine Maude model checking with Athena natural-deduction proofs for properties beyond rewriting reach.
  • Parametric induction rules allow direct reasoning about data types defined with structural axioms without separate encodings.
  • The approach stays practical for common specifications that meet the conditions for compactness.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Hybrid verification tools could automate switching between Maude execution and Athena proofs for the same specification.
  • The compactness result suggests the method could handle realistic industrial-scale equational modules without manual simplification.
  • Similar translations might be developed for other rewriting-logic languages to add inductive support.

Load-bearing premise

The translation preserves the semantics of the original Maude specification while remaining compact and suitable for deductive reasoning.

What would settle it

A Maude equational theory where the Athena version either fails to prove a property true in the original or proves a property false in the original, or where the translated theory size grows exponentially for a standard specification using associativity and commutativity.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper introduces maude2athena, a translation framework that converts Maude equational theories (order-sorted signatures, equations modulo axioms such as associativity/commutativity/identity) into Athena specifications. It claims to support natural-deduction proofs including induction with parametric rules, equational chaining, and case analysis while faithfully encoding membership equational logic in a many-sorted setting, preserving semantics, and avoiding exponential blowup under reasonable conditions.

Significance. If the translation is shown to be faithful and compact, the work would usefully connect Maude's executable rewriting logic with Athena's inductive theorem-proving facilities, enabling combined execution and proof-based verification. The emphasis on parametric induction rules for structural axioms is a potentially valuable technical feature for avoiding manual axiom instantiation.

major comments (1)
  1. [Abstract] Abstract: the central claims of faithful semantic preservation, support for induction modulo axioms, and absence of exponential blowup are asserted without any translation rules, example derivations, or proof sketches. This prevents assessment of whether the encoding is load-bearing for the stated properties.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the review and for highlighting the need for clearer linkage between the abstract claims and the supporting technical content. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claims of faithful semantic preservation, support for induction modulo axioms, and absence of exponential blowup are asserted without any translation rules, example derivations, or proof sketches. This prevents assessment of whether the encoding is load-bearing for the stated properties.

    Authors: The abstract is deliberately concise and follows standard conventions by summarizing contributions at a high level rather than embedding full technical artifacts. The manuscript body supplies the requested material: translation rules appear in Section 3, concrete example derivations (including induction modulo associativity/commutativity) are given in Section 4, and proof sketches establishing semantic preservation together with the conditions under which the translation remains compact (no exponential blowup) are provided in Section 5. These sections collectively demonstrate that the encoding is load-bearing for the stated properties. If the referee believes the abstract would benefit from explicit forward references to these sections, we are prepared to add one or two sentences to that effect. revision: partial

Circularity Check

0 steps flagged

No significant circularity detected in translation framework

full rationale

The paper presents maude2athena as a systematic translation from Maude equational theories (with membership equational logic and structural axioms) into Athena for natural deduction, inductive reasoning, and equational chaining. The central claims—semantic preservation, support for induction modulo axioms via parametric rules, and compactness without exponential blowup—are justified by the explicit design of the translation mappings and their stated properties under reasonable conditions, rather than by any self-definitional loop, fitted parameter renamed as prediction, or load-bearing self-citation chain. No derivation step reduces a claimed result to its own inputs by construction; the work is a tool-building contribution relying on the independent semantics of the source and target systems.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that membership equational logic can be faithfully and compactly encoded into many-sorted first-order logic with induction.

axioms (1)
  • domain assumption Membership equational logic can be encoded in many-sorted first-order logic without exponential blowup under reasonable conditions
    Invoked to justify the translation's compactness and faithfulness.

pith-pipeline@v0.9.0 · 5503 in / 1037 out tokens · 51695 ms · 2026-05-10T01:33:44.891690+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

30 extracted references · 30 canonical work pages

  1. [1]

    Theoretical com- puter science (1992) Equational and Inductive Reasoning for Maude in Athena 19

    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical com- puter science (1992) Equational and Inductive Reasoning for Maude in Athena 19

    work page 1992

  2. [2]

    Springer (2007)

    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All about Maude-a high-performance logical framework: how to specify, program, and verify systems in rewriting logic. Springer (2007)

    work page 2007

  3. [3]

    Theoretical Computer Science (2007)

    Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. Theoretical Computer Science (2007)

    work page 2007

  4. [4]

    MIT Press (2017)

    Arkoudas, K., Musser, D.: Fundamental proof methods in computer science: a computer-based approach. MIT Press (2017)

    work page 2017

  5. [5]

    In: Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation

    Li, L., Gunter, E.L.: A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras. In: Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation. EPTCS, pp. 20–34 (2017)

    work page 2017

  6. [6]

    Theoretical Computer Science (1992)

    Goguen, J.A., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheri- tance, overloading, exceptions and partial operations. Theoretical Computer Science (1992)

    work page 1992

  7. [7]

    In: Logic for Programming, Artificial Intelligence, and Reasoning, pp

    Rocha, C., Meseguer, J.: Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories. In: Logic for Programming, Artificial Intelligence, and Reasoning, pp. 594–

    work page

  8. [8]

    Theoretical Computer Science (2000)

    Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science (2000)

    work page 2000

  9. [9]

    In: Recent Trends in Algebraic Development Techniques, pp

    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Recent Trends in Algebraic Development Techniques, pp. 18–61. Springer (1998)

    work page 1998

  10. [10]

    The Journal of Logic and Algebraic Programming (2012)

    Durán, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order- sorted rewrite theories. The Journal of Logic and Algebraic Programming (2012)

    work page 2012

  11. [11]

    Electronic Notes in Theoretical Computer Science (2009)

    Lucas,S.,Meseguer,J.:Operationalterminationofmembershipequationalprograms:theorder- sorted way. Electronic Notes in Theoretical Computer Science (2009)

    work page 2009

  12. [12]

    PhD thesis, Massachusetts Institute of Technology (2000)

    Arkoudas, K.: Denotational proof languages. PhD thesis, Massachusetts Institute of Technology (2000)

    work page 2000

  13. [13]

    Journal of Auto- mated Reasoning (2005)

    Arkoudas, K.: Simplifying Proofs in Fitch-Style Natural Deduction Systems. Journal of Auto- mated Reasoning (2005)

    work page 2005

  14. [14]

    Cambridge University Press (1996)

    Manzano, M.: Extensions of first-order logic. Cambridge University Press (1996)

    work page 1996

  15. [15]

    In: Proceedings of the 2013 Workshop on Programming Based on Actors, Agents, and Decentralized Control

    Musser, D.R., Varela, C.A.: Structured Reasoning About Actor Systems. In: Proceedings of the 2013 Workshop on Programming Based on Actors, Agents, and Decentralized Control. AGERE! 2013, pp. 37–48. ACM, Indianapolis, Indiana, USA (2013)

    work page 2013

  16. [16]

    The AMST Language: Formal Verification and Execution of Actor Systems

    Varela, C.A.: “The AMST Language: Formal Verification and Execution of Actor Systems”. In: Concurrent Programming, Open Systems and Formal Methods: Essays Dedicated to Gul Agha to Celebrate His Scientific Career. Cham: Springer Nature Switzerland, 2026, pp. 36–59

    work page 2026

  17. [17]

    Science of Computer Programming (2025)

    Paul, S., McCarthy, C., Patterson, S., Varela, C.: Formal verification of timely knowledge prop- agation in airborne networks. Science of Computer Programming (2025)

    work page 2025

  18. [18]

    IEEE Aerospace and Electronic Systems Magazine (2023)

    Paul, S., Cruz, E., Dutta, A., Bhaumik, A., Blasch, E., Agha, G., Patterson, S., Kopsaftopoulos, F., Varela, C.: Formal Verification of Safety-Critical Aerospace Systems. IEEE Aerospace and Electronic Systems Magazine (2023)

    work page 2023

  19. [19]

    Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Form. Asp. Comput. (2017)

    work page 2017

  20. [20]

    In: International Conference on Theorem Proving in Higher Order Logics, pp

    Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: International Conference on Theorem Proving in Higher Order Logics, pp. 33–38 (2008)

    work page 2008

  21. [21]

    In: Interna- tional Conference on Automated Deduction, pp

    Moura, L.d., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Interna- tional Conference on Automated Deduction, pp. 625–635 (2021) 20 M.Sanabria et al

    work page 2021

  22. [22]

    In: International Symposium on Principles and Practice of Declarative Programming, pp

    Durán, F., Escobar, S., Meseguer, J., Sapiña, J.: NuITP: An inductive theorem prover for equational program verification. In: International Symposium on Principles and Practice of Declarative Programming, pp. 1–11 (2024)

    work page 2024

  23. [23]

    Theory and Practice of Logic Programming (2021)

    Bringsjord, S., Govindarajulu, N.S.: Fundamental Proof Methods in Computer Science: A Computer-Based Approach, by Arkoudas and Musser, The MIT Press, Cambridge, USA, ISBN 978-0-262-03553-8. Theory and Practice of Logic Programming (2021)

    work page 2021

  24. [24]

    In: International Workshop on Rewriting Logic and its Applications, pp

    Rocha, C., Meseguer, J., Muñoz, C.: Rewriting modulo SMT and open system analysis. In: International Workshop on Rewriting Logic and its Applications, pp. 247–262 (2014)

    work page 2014

  25. [25]

    In: NASA Formal Methods, pp

    Romero, M.,Rocha, C.: Symbolic Executionand Reachability AnalysisUsing RewritingModulo SMT for Spatial Concurrent Constraint Systems with Extrusion. In: NASA Formal Methods, pp. 435–451. Springer (2018)

    work page 2018

  26. [26]

    In: International Conference on Applications and Theory of Petri Nets and Concurrency, pp

    Arias, J., Bae, K., Olarte, C., Ölveczky, P.C., Petrucci, L., Rømming, F.: Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving. In: International Conference on Applications and Theory of Petri Nets and Concurrency, pp. 369–392 (2023)

    work page 2023

  27. [27]

    In: International Conference on Algebraic Methodology and Software Technology, pp

    Codescu, M., Mossakowski, T., Riesco, A., Maeder, C.: Integrating Maude into HETS. In: International Conference on Algebraic Methodology and Software Technology, pp. 60–75 (2010)

    work page 2010

  28. [28]

    Theoretical Computer Science (2002)

    Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: the common algebraic specification language. Theoretical Computer Science (2002)

    work page 2002

  29. [29]

    Journal of Logical and Algebraic Methods in Programming (2022)

    Rubio, R., Riesco, A.: Maude2Lean: Theorem proving for Maude specifications using Lean. Journal of Logical and Algebraic Methods in Programming (2022)

    work page 2022

  30. [30]

    Theoretical Computer Science (2002)

    Talcott, C.: Actor theories in rewriting logic. Theoretical Computer Science (2002)

    work page 2002