Specification and proof in membership equational logic
From MaRDI portal
Publication:1978640
DOI10.1016/S0304-3975(99)00206-6zbMath0938.68057OpenAlexW1991598919WikidataQ128026434 ScholiaQ128026434MaRDI QIDQ1978640
Adel Bouhoula, Jean-Pierre Jouannaud, José Meseguer
Publication date: 4 June 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(99)00206-6
Related Items
Rewriting logic: Roadmap and bibliography, Executable structural operational semantics in Maude, Unnamed Item, Algebraic simulations, Declarative Debugging of Rewriting Logic Specifications, Order-Sorted Parameterization and Induction, On the Specification and Verification of Model Transformations, Proving termination of context-sensitive rewriting by transformation, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, The rewriting logic semantics project, Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types, A probabilistic approximate logic for neuro-symbolic learning and reasoning, José Meseguer: Scientist and Friend Extraordinaire, Two Decades of Maude, Parameterized strategies specification in Maude, Twenty years of rewriting logic, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Declarative debugging of rewriting logic specifications, Modular rewritable Petri nets: an efficient model for dynamic distributed systems, Declarative Debugging of Membership Equational Logic Specifications, Sufficient completeness verification for conditional and constrained TRS, Canonization of reconfigurable PT nets in \texttt{Maude}, Verification of the ROS NavFn planner using executable specification languages, A generic framework for \(n\)-protocol compatibility checking, MTT: The Maude Termination Tool (System Description), Automated Induction with Constrained Tree Automata, Unnamed Item, Unnamed Item, Specification and proof in membership equational logic, Equational abstractions, Travelling salesman problem in tissue P systems with costs, Strategies, model checking and branching-time properties in Maude, Resource provisioning strategies for BPMN processes: specification and analysis using Maude, Strict coherence of conditional rewriting modulo axioms, A Maude environment for CafeOBJ, Strategy-Based Rewrite Semantics for Membrane Systems Preserves Maximal Concurrency of Evolution Rule Actions, Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework, An algebraic semantics for MOF, Memory Policy Analysis for Semantics Specifications in Maude, A Declarative Debugger for Maude Functional Modules, Operational Termination of Membership Equational Programs: the Order-Sorted Way, Proving operational termination of membership equational programs, Semantic foundations for generalized rewrite theories, Inductive-data-type systems, Integrating Maude into Hets, Programming and symbolic computation in Maude, Ground confluence of order-sorted conditional specifications modulo axioms, Methods for Proving Termination of Rewriting-based Programming Languages by Transformation, Order-Sorted Rewriting and Congruence Closure, Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*, Interpreting Abstract Interpretations in Membership Equational Logic, Towards Behavioral Maude, Operational termination of conditional term rewriting systems, Formal Analysis of Leader Election in MANETs Using Real-Time Maude, Automata-driven automated induction, Functorial models for Petri nets, Coding Mobile Synchronizing Petri Nets into Rewriting Logic, Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics, Abstraction and Model Checking of Core Erlang Programs in Maude, Maude: specification and programming in rewriting logic, Reflection in conditional rewriting logic, Symbolic computation in Maude: some tapas
Uses Software
Cites Work
- Using induction and rewriting to verify and complete parameterized specifications
- Equational type logic
- A completion procedure for conditional equations
- Proofs by induction in equational theories with constructors
- Parametrization for order-sorted algebraic specification
- Equational completion in order-sorted algebras
- A rationale for conditional equational programming
- Conditional rewrite rules
- Reductions in tree replacement systems
- Mechanizing structural induction. II: Strategies
- Order-sorted completion: The many-sorted way
- Conditional rewriting logic as a unified model of concurrency
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- The algebraic specification of abstract data types
- Completion of rewrite systems with membership constraints. I: Deduction rules
- Dynamically typed computations for order-sorted equational presentations
- Equational formulae with membership constraints
- Automated theorem proving by test set induction
- May I borrow your logic? (Transporting logical structures along maps)
- Abstract data type systems
- Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
- A strong restriction of the inductive completion procedure
- Automatic proofs by induction in theories without constructors
- Partial algebras-survey of a unifying approach towards a two-valued model theory for partial algebras
- Automata-driven automated induction
- Ground reducibility is EXPTIME-complete
- Implicit induction in conditional theories
- Tree automata help one to solve equational formulae in AC-theories
- Specification and proof in membership equational logic
- Lokal präsentierbare Kategorien. (Locally presentable categories)
- Completion of a Set of Rules Modulo a Set of Equations
- Programming with equalities, subsorts, overloading, and parametrization in OBJ
- Abstract data types and software validation
- Pumping, cleaning and symbolic constraints solving
- Inclusions and subtypes I: first-order case
- Inclusions and subtypes II: higher-order case
- Inductive proofs by specification transformations
- Detecting redundant narrowing derivations by the LSE-SL reducibility test
- Encompassment properties and automata with constraints
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
