scientific article; zbMATH DE number 177848

MaRDI QIDQ4038726zbMATH OpenFDO

Authors Hubert Comon

Publication date 18 May 1993

zbMATH Keywords

equational theoriesalgebraic specificationfirst order theoryregular tree languagesort constraintsrational tree languageautomatic inductive proofsequations between termstransformation rules for first order formulas

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Decidability of theories and sets of sentences (03B25) Abstract data types; algebraic specification (68Q65)

Recommendations

• Equational formulae with membership constraints
• scientific article; zbMATH DE number 3949706
• Equational formulas and pattern operations in initial order-sorted algebras
• Equational formulas and pattern operations in initial order-sorted algebras
• Inductive proofs by specification transformations

Cited in

(21)

• Generalized rewrite theories, coherence completion, and symbolic methods
• Complete axiomatizations of some quotient term algebras
• Completion of rewrite systems with membership constraints
• Equational formulas and pattern operations in initial order-sorted algebras
• Recognizable tree-languages and nonlinear morphisms
• Equational formulas and pattern operations in initial order-sorted algebras
• Encompassment properties and automata with constraints
• Metalevel algorithms for variant satisfiability
• A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
• scientific article; zbMATH DE number 1231543 (Why is no real title available?)
• Confluence of terminating membership conditional TRS
• Unification in sort theories and its applications
• Set constraints and automata
• Equational formulae with membership constraints
• Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
• Equational completion in order-sorted algebras
• Semantics of order-sorted specifications
• A method for simultaneous search for refutations and models by equational constraint solving
• The first order theory of primal grammars is decidable
• Pumping, cleaning and symbolic constraints solving
• Regular substitution sets: A means of controlling E-unification

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4038726)