Complete axiomatizations of some quotient term algebras

DOI10.1016/0304-3975(93)90108-6zbMath0810.03026MaRDI 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 theory; existential fragment of the theory of associative-commutative function symbols; quasi-free theory

Mathematics Subject Classification ID

08A70: Applications of universal algebra in computer science

03B25: Decidability of theories and sets of sentences

03C05: Equational classes, universal algebra in model theory

08C10: Axiomatic model classes

03C10: Quantifier elimination, model completeness, and related topics

Related Items

Complete axiomatizations of some quotient term algebras, Representing and building models for decidable subclasses of equational clausal logic, The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable., Congruential complements of ground term rewrite systems

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