Equational formulae with membership constraints

DOI10.1006/inco.1994.1056zbMath0827.03020OpenAlexW1964783683MaRDI QIDQ1333268

Catherine Delor, Hubert Comon

Publication date: 13 December 1995

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1994.1056

zbMATH Keywords

solvabilityaxiomatizationregular tree languageorder-sorted algebrasautomatic proofs by induction in equational theoriesequational formulaemembership constraintsunifier

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Equational classes, universal algebra in model theory (03C05) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (24)

Equational formulas and pattern operations in initial order-sorted algebras ⋮ Equational and membership constraints for infinite trees ⋮ Extension of the associative path ordering to a chain of associative commutative symbols ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Equality and disequality constraints on direct subterms in tree automata ⋮ Unification of infinite sets of terms schematized by primal grammars ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ On the complexity of equational problems in CNF ⋮ Decision procedures for term algebras with integer constraints ⋮ Tree Automata with Global Constraints ⋮ Specification and proof in membership equational logic ⋮ Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras ⋮ On deciding subsumption problems ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Predicate Completion for non-Horn Clause Sets ⋮ Classes of Tree Homomorphisms with Decidable Preservation of Regularity ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Regular expression order-sorted unification and matching ⋮ How to win a game with features ⋮ Invariant Checking for Programs with Procedure Calls ⋮ Explicit versus implicit representations of subsets of the Herbrand universe. ⋮ Sequentiality, monadic second-order logic and tree automata. ⋮ Automata-driven automated induction

This page was built for publication: Equational formulae with membership constraints