A Unification Algorithm for Associative-Commutative Functions
From MaRDI portal
Publication:3912070
DOI10.1145/322261.322262zbMath0462.68075OpenAlexW2033288425WikidataQ56609900 ScholiaQ56609900MaRDI QIDQ3912070
Publication date: 1981
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322261.322262
Related Items
Completion procedures as semidecision procedures, Mark Stickel: his earliest work, Semantically-guided goal-sensitive reasoning: model representation, Unification in partially commutative semigroups, Automated deduction with associative-commutative operators, Alternating two-way AC-tree automata, On unification: Equational theories are not bounded, History and Prospects for First-Order Automated Deduction, Complete sets of reductions modulo associativity, commutativity and identity, Consider only general superpositions in completion procedures, Simulating Buchberger's algorithm by Knuth-Bendix completion, AC-complete unification and its application to theorem proving, Complexity of matching problems, Associative-commutative unification, Unification in combinations of collapse-free regular theories, An algebraic approach to unification under associativity and commutativity, Embedding Boolean expressions into logic programming, History and basic features of the critical-pair/completion procedure, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Unnamed Item, Unification in commutative idempotent monoids, Efficient solution of linear diophantine equations, Permutative rewriting and unification, Combination of constraint solvers for free and quasi-free structures, Unnecessary inferences in associative-commutative completion procedures, Unification properties of commutative theories: A categorical treatment, Modular AC unification of higher-order patterns, “Syntactic” AC-unification, Avoiding slack variables in the solving of linear diophantine equations and inequations, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, Ramification and causality, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, Unification of drags and confluence of drag rewriting, Nominal AC-matching, On the unification problem for Cartesian closed categories, Completion for unification, Linear groupoids and the associated wreath products., Towards a foundation of completion procedures as semidecision procedures, Unification algorithms cannot be combined in polynomial time, Unification theory, AC-unification race: The system solving approach, implementation and benchmarks, Complexity of unification problems with associative-commutative operators, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, A new method for undecidability proofs of first order theories, On the complexity of deduction modulo leaf permutative equations, AC unification through order-sorted AC1 unification, Building Theorem Provers, Unification in commutative theories, Unification in Boolean rings and Abelian groups, Unification in a combination of arbitrary disjoint equational theories, On the complexity of recognizing the Hilbert basis of a linear Diophantine system, On the parameterized complexity of associative and commutative unification, On pot, pans and pudding or how to discover generalised critical Pairs, Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques, Completion for rewriting modulo a congruence, Adventures in associative-commutative unification, Complete sets of unifiers and matchers in equational theories, Unification problem in equational theories, Unification in permutative equational theories is undecidable, Type dependencies for logic programs using ACI-unification, A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs, Unification algorithms cannot be combined in polynomial time., A superposition oriented theorem prover, Refutational theorem proving using term-rewriting systems, Competing for the \(AC\)-unification race
