Specification and proof in membership equational logic
type: Item
instance of: scholarly article
title: Specification and proof in membership equational logic
zbMATH Open document ID: 0938.68057
DOI: 10.1016/S0304-3975(99)00206-6
author: Adel Bouhoula
author: Jean-Pierre Jouannaud
author: José Meseguer
published in: Theoretical Computer Science
publication date: 2000-06-04T00:00:00Z
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 1454398
zbMATH Keywords: executable algebraic specifications
zbMATH Keywords: parameterized modules
zbMATH Keywords: inductive proofs
describes a project that uses: OBJ3
describes a project that uses: Maude
describes a project that uses: NQTHM
MaRDI profile type: Publication
cites work: Mechanizing structural induction. II: Strategies
cites work: Q3682648
cites work: Q3896478
cites work: Q4264712
cites work: Using induction and rewriting to verify and complete parameterized specifications
cites work: Automated theorem proving by test set induction
cites work: Automata-driven automated induction
cites work: Implicit induction in conditional theories
cites work: Q3835049
cites work: Partial algebras-survey of a unifying approach towards a two-valued model theory for partial algebras
cites work: Pumping, cleaning and symbolic constraints solving
cites work: Encompassment properties and automata with constraints
cites work: May I borrow your logic? (Transporting logical structures along maps)
cites work: Q3785921
cites work: Q3490949
cites work: Inductive proofs by specification transformations
cites work: Completion of rewrite systems with membership constraints. I: Deduction rules
cites work: Equational formulae with membership constraints
cites work: Q4942651
cites work: Q3855354
cites work: Q4385532
cites work: A rationale for conditional equational programming
cites work: Q3817652
cites work: Ground reducibility is EXPTIME-complete
cites work: A strong restriction of the inductive completion procedure
cites work: Lokal präsentierbare Kategorien. (Locally presentable categories)
cites work: Reductions in tree replacement systems
cites work: A completion procedure for conditional equations
cites work: Order-sorted completion: The many-sorted way
cites work: Equational completion in order-sorted algebras
cites work: Q3719824
cites work: Q3030249
cites work: Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
cites work: Abstract data types and software validation
cites work: The algebraic specification of abstract data types
cites work: Dynamically typed computations for order-sorted equational presentations
cites work: Proofs by induction in equational theories with constructors
cites work: Q3883561
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Q4297316
cites work: Programming with equalities, subsorts, overloading, and parametrization in OBJ
cites work: Automatic proofs by induction in theories without constructors
cites work: Abstract data type systems
cites work: Conditional rewrite rules
cites work: Q3795207
cites work: Q3338226
cites work: Q3690200
cites work: Detecting redundant narrowing derivations by the LSE-SL reducibility test
cites work: Tree automata help one to solve equational formulae in AC-theories
cites work: Q4222853
cites work: Equational type logic
cites work: Inclusions and subtypes I: first-order case
cites work: Inclusions and subtypes II: higher-order case
cites work: Q3032225
cites work: Conditional rewriting logic as a unified model of concurrency
cites work: Q3839051
cites work: Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
cites work: Q3204056
cites work: Parametrization for order-sorted algebraic specification
full work available at URL: s0304-3975(99)00206-6
OpenAlex ID: W1991598919

Specification and proof in membership equational logic (cites work)
cites work: Specification and proof in membership equational logic

Specification and proof in membership equational logic (Wikidata QID)
Wikidata QID: Q128026434