Pages that link to "Item:Q3912070"
From MaRDI portal
The following pages link to A Unification Algorithm for Associative-Commutative Functions (Q3912070):
Displaying 20 items.
- Simulating Buchberger's algorithm by Knuth-Bendix completion (Q5055776) (← links)
- AC-complete unification and its application to theorem proving (Q5055849) (← links)
- Unification properties of commutative theories: A categorical treatment (Q5096265) (← links)
- Modular AC unification of higher-order patterns (Q5096303) (← links)
- “Syntactic” AC-unification (Q5096305) (← links)
- Building Theorem Provers (Q5191110) (← links)
- On pot, pans and pudding or how to discover generalised critical Pairs (Q5210806) (← links)
- (Q5216313) (← links)
- A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs (Q5504662) (← links)
- Completion procedures as semidecision procedures (Q5881279) (← links)
- On the complexity of recognizing the Hilbert basis of a linear Diophantine system (Q5958323) (← links)
- When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus (Q6041667) (← links)
- Complete equational unification based on an extension of the Knuth-Bendix completion procedure (Q6114511) (← links)
- Unification theory (Q6169561) (← links)
- Some results on equational unification (Q6488537) (← links)
- Unification in a combination of equational theories: an efficient algorithm (Q6488538) (← links)
- Complete sets of reductions with constraints (Q6488546) (← links)
- Retrieving library identifiers via equational matching of types (Q6488563) (← links)
- Unification in monoidal theories (Q6488564) (← links)
- Positive deduction modulo regular theories (Q6560184) (← links)
