The negation elimination from syntactic equational formula is decidable

DOI10.1007/978-3-662-21551-7_24zbMATH Open1503.03009OpenAlexW44081821MaRDI QIDQ5055804FDOQ5055804

Mohamed Tajine

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-21551-7_24

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Decidability of theories and sets of sentences (03B25) Equational classes, universal algebra in model theory (03C05)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear unification
• An Efficient Unification Algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• The algebraic specification of abstract data types
• Automatic proofs by induction in theories without constructors
• Explicit representation of terms defined by counter examples
• An almost linear Robinson unification algorithm

Cited In (5)

• Explicit versus implicit representations of subsets of the Herbrand universe.
• Equational formulas and pattern operations in initial order-sorted algebras
• More problems in rewriting
• Title not available (Why is that?)
• Title not available (Why is that?)

   Recommendations

• Title not available (Why is that?) 👍 👎
• Negation elimination in equational formulae 👍 👎
• Negation elimination in empty or permutative theories 👍 👎
• AC complement problems: Satisfiability and negation elimination 👍 👎
• Title not available (Why is that?) 👍 👎

This page was built for publication: The negation elimination from syntactic equational formula is decidable

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