Specification and proof in membership equational logic
From MaRDI portal
Publication:1978640
DOI10.1016/S0304-3975(99)00206-6zbMATH Open0938.68057OpenAlexW1991598919WikidataQ128026434 ScholiaQ128026434MaRDI QIDQ1978640FDOQ1978640
Recommendations
- Maude: specification and programming in rewriting logic
- scientific article; zbMATH DE number 1189278
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- scientific article; zbMATH DE number 1615226
- scientific article; zbMATH DE number 1231659
Cites Work
- scientific article; zbMATH DE number 4018380 (Why is no real title available?)
- scientific article; zbMATH DE number 4130339 (Why is no real title available?)
- scientific article; zbMATH DE number 4180819 (Why is no real title available?)
- scientific article; zbMATH DE number 3871335 (Why is no real title available?)
- scientific article; zbMATH DE number 4164137 (Why is no real title available?)
- scientific article; zbMATH DE number 3904807 (Why is no real title available?)
- scientific article; zbMATH DE number 3913659 (Why is no real title available?)
- scientific article; zbMATH DE number 3949706 (Why is no real title available?)
- scientific article; zbMATH DE number 4049024 (Why is no real title available?)
- scientific article; zbMATH DE number 4060701 (Why is no real title available?)
- scientific article; zbMATH DE number 4090847 (Why is no real title available?)
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 3656176 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3703962 (Why is no real title available?)
- scientific article; zbMATH DE number 1231537 (Why is no real title available?)
- scientific article; zbMATH DE number 1348460 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1414314 (Why is no real title available?)
- A completion procedure for conditional equations
- A rationale for conditional equational programming
- A strong restriction of the inductive completion procedure
- Abstract data type systems
- Abstract data types and software validation
- Automata-driven automated induction
- Automated theorem proving by test set induction
- Automatic proofs by induction in theories without constructors
- Completion of a Set of Rules Modulo a Set of Equations
- Completion of rewrite systems with membership constraints. I: Deduction rules
- Conditional rewrite rules
- Conditional rewriting logic as a unified model of concurrency
- Detecting redundant narrowing derivations by the LSE-SL reducibility test
- Dynamically typed computations for order-sorted equational presentations
- Encompassment properties and automata with constraints
- Equational completion in order-sorted algebras
- Equational formulae with membership constraints
- Equational type logic
- Ground reducibility is EXPTIME-complete
- Implicit induction in conditional theories
- Inclusions and subtypes I: first-order case
- Inclusions and subtypes II: higher-order case
- Inductive proofs by specification transformations
- Lokal präsentierbare Kategorien. (Locally presentable categories)
- May I borrow your logic? (Transporting logical structures along maps)
- Mechanizing structural induction. II: Strategies
- Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Order-sorted completion: The many-sorted way
- Parametrization for order-sorted algebraic specification
- Partial algebras-survey of a unifying approach towards a two-valued model theory for partial algebras
- Programming with equalities, subsorts, overloading, and parametrization in OBJ
- Proofs by induction in equational theories with constructors
- Pumping, cleaning and symbolic constraints solving
- Reductions in tree replacement systems
- Specification and proof in membership equational logic
- The algebraic specification of abstract data types
- Tree automata help one to solve equational formulae in AC-theories
- Using induction and rewriting to verify and complete parameterized specifications
Cited In (71)
- A tutorial on specifying data structures in Maude
- Maude2Lean: theorem proving for Maude specifications using Lean
- Towards behavioral Maude: behavioral membership equational logic
- José Meseguer: scientist and friend extraordinaire
- Formalization and analysis of the post-quantum signature scheme FALCON with Maude
- Memory policy analysis for semantics specifications in 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
- Operational termination of membership equational programs: the order-sorted way
- Twenty years of rewriting logic
- Strict coherence of conditional rewriting modulo axioms
- Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions
- 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
- 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 no real title available?)
- Automated Induction with Constrained Tree Automata
- MTT: The Maude Termination Tool (System Description)
- Order-sorted equality enrichments modulo axioms
- 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 no real title available?)
- Methods for proving termination of rewriting-based programming languages by transformation
- Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework
- A Church-Rosser checker tool for conditional order-sorted equational Maude specifications
- Parameterized strategies specification in Maude
- Algebraic simulations
- Programming and symbolic computation in Maude
- On the Specification and Verification of Model Transformations
- Formal analysis of leader election in MANETs using Real-Time Maude
- Functional logic programming in Maude
- Title not available (Why is no real title available?)
- Equational abstractions
- Functional and Logic Programming
- A declarative debugger for Maude functional modules
- Sufficient completeness verification for conditional and constrained TRS
- Order-Sorted Parameterization and Induction
- Title not available (Why is no real title available?)
- 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
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)
