Complete axiomatizations of some quotient term algebras

DOI10.1016/0304-3975(93)90108-6zbMath0810.03026OpenAlexW2070687667MaRDI QIDQ685393

Hubert Comon

Publication date: 20 April 1995

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(93)90108-6

zbMATH Keywords

first-order theoryexistential fragment of the theory of associative-commutative function symbolsquasi-free theory

Mathematics Subject Classification ID

Applications of universal algebra in computer science (08A70) Decidability of theories and sets of sentences (03B25) Equational classes, universal algebra in model theory (03C05) Axiomatic model classes (08C10) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (12)

Problems in rewriting III ⋮ Unnamed Item ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Metalevel algorithms for variant satisfiability ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable. ⋮ Complete axiomatizations of some quotient term algebras ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ Congruential complements of ground term rewrite systems ⋮ Formalising nominal C-unification generalised with protected variables

Cites Work

• Complete axiomatizations of some quotient term algebras
• Equational problems and disunification
• Decidability of the existential theory of infinite terms with subterm relation
• Proving termination with multiset orderings
• Fast Decision Procedures Based on Congruence Closure
• Higher-order unification, polymorphism, and subsorts
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Complete axiomatizations of some quotient term algebras