Specification and proof in membership equational logic
From MaRDI portal
Publication:1978640
DOI10.1016/S0304-3975(99)00206-6zbMATH Open0938.68057OpenAlexW1991598919WikidataQ128026434 ScholiaQ128026434MaRDI QIDQ1978640FDOQ1978640
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
Recommendations
Cites Work
- Lokal präsentierbare Kategorien. (Locally presentable categories)
- Title not available (Why is that?)
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Conditional rewrite rules
- Conditional rewriting logic as a unified model of concurrency
- Title not available (Why is that?)
- A rationale for conditional equational programming
- Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
- Title not available (Why is that?)
- Partial algebras-survey of a unifying approach towards a two-valued model theory for partial algebras
- The algebraic specification of abstract data types
- Automata-driven automated induction
- Ground reducibility is EXPTIME-complete
- Implicit induction in conditional theories
- Specification and proof in membership equational logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Using induction and rewriting to verify and complete parameterized specifications
- Proofs by induction in equational theories with constructors
- Title not available (Why is that?)
- Completion of a Set of Rules Modulo a Set of Equations
- Automatic proofs by induction in theories without constructors
- Encompassment properties and automata with constraints
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Abstract data types and software validation
- A strong restriction of the inductive completion procedure
- Mechanizing structural induction. II: Strategies
- Title not available (Why is that?)
- Pumping, cleaning and symbolic constraints solving
- Equational type logic
- A completion procedure for conditional equations
- Completion of rewrite systems with membership constraints. I: Deduction rules
- Inclusions and subtypes II: higher-order case
- Inductive proofs by specification transformations
- Equational formulae with membership constraints
- Title not available (Why is that?)
- Reductions in tree replacement systems
- Title not available (Why is that?)
- May I borrow your logic? (Transporting logical structures along maps)
- Abstract data type systems
- Automated theorem proving by test set induction
- Tree automata help one to solve equational formulae in AC-theories
- Order-sorted completion: The many-sorted way
- Parametrization for order-sorted algebraic specification
- Equational completion in order-sorted algebras
- Title not available (Why is that?)
- Title not available (Why is that?)
- Programming with equalities, subsorts, overloading, and parametrization in OBJ
- Dynamically typed computations for order-sorted equational presentations
- Inclusions and subtypes I: first-order case
- Title not available (Why is that?)
- Detecting redundant narrowing derivations by the LSE-SL reducibility test
Cited In (67)
- Memory Policy Analysis for Semantics Specifications in Maude
- Maude2Lean: theorem proving for Maude specifications using Lean
- Formalization and analysis of the post-quantum signature scheme FALCON with Maude
- Coding mobile synchronizing Petri nets into rewriting logic
- Modular rewritable Petri nets: an efficient model for dynamic distributed systems
- Canonization of reconfigurable PT nets in \texttt{Maude}
- Travelling salesman problem in tissue P systems with costs
- Twenty years of rewriting logic
- Strict coherence of conditional rewriting modulo axioms
- Functorial models for Petri nets
- Symbolic computation in Maude: some tapas
- Inductive-data-type systems
- Reflection in conditional rewriting logic
- Ground confluence of order-sorted conditional specifications modulo axioms
- The rewriting logic semantics project
- Proving operational termination of membership equational programs
- An algebraic semantics for MOF
- Semantic foundations for generalized rewrite theories
- Declarative Debugging of Rewriting Logic Specifications
- Formal Analysis of Leader Election in MANETs Using Real-Time Maude
- Resource provisioning strategies for BPMN processes: specification and analysis using Maude
- Proving termination of context-sensitive rewriting by transformation
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Title not available (Why is that?)
- A Declarative Debugger for Maude Functional Modules
- Automated Induction with Constrained Tree Automata
- MTT: The Maude Termination Tool (System Description)
- Strategies, model checking and branching-time properties in Maude
- Abstraction and model checking of core Erlang programs in Maude
- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
- Executable structural operational semantics in Maude
- A generic framework for \(n\)-protocol compatibility checking
- Automata-driven automated induction
- Integrating Maude into Hets
- Specification and proof in membership equational logic
- Title not available (Why is that?)
- Methods for proving termination of rewriting-based programming languages by transformation
- Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework
- Parameterized strategies specification in Maude
- Algebraic simulations
- Programming and symbolic computation in Maude
- Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
- On the Specification and Verification of Model Transformations
- Equational abstractions
- Operational Termination of Membership Equational Programs: the Order-Sorted Way
- Functional and Logic Programming
- José Meseguer: Scientist and Friend Extraordinaire
- Strategy-Based Rewrite Semantics for Membrane Systems Preserves Maximal Concurrency of Evolution Rule Actions
- Sufficient completeness verification for conditional and constrained TRS
- Towards behavioral Maude: behavioral membership equational logic
- Order-Sorted Parameterization and Induction
- Title not available (Why is that?)
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Interpreting abstract interpretations in membership equational logic
- Verification of the ROS NavFn planner using executable specification languages
- Maude: specification and programming in rewriting logic
- Operational termination of conditional term rewriting systems
- A probabilistic approximate logic for neuro-symbolic learning and reasoning
- Order-Sorted Rewriting and Congruence Closure
- CINNI -- a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi
- Checking Sufficient Completeness by Inductive Theorem Proving
- Two Decades of Maude
- Rewriting logic: Roadmap and bibliography
- A Maude environment for CafeOBJ
- Using Maude and its strategies for defining a framework for analyzing Eden semantics
- Declarative Debugging of Membership Equational Logic Specifications
- Declarative debugging of rewriting logic specifications
Uses Software
This page was built for publication: Specification and proof in membership equational logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1978640)
