Unification theory

DOI10.1016/S0747-7171(89)80012-4zbMath0678.68098OpenAlexW2914314632MaRDI QIDQ1124375

Jörg H. Siekmann

Publication date: 1989

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(89)80012-4

zbMATH Keywords

Unification theory

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

Related Items (64)

Semi-unification of two terms in Abelian groups ⋮ Unification in partially commutative semigroups ⋮ Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification ⋮ Undecidable properties of syntactic theories ⋮ An algorithm for distributive unification ⋮ Implementation of a UU-algorithm for primitive recursive tree functions ⋮ A formal semantics for DAI language NUML ⋮ The Kreisel length-of-proof problem ⋮ Incremental constraint satisfaction for equational logic programming ⋮ Unification, finite duality and projectivity in varieties of Heyting algebras ⋮ E-Unification based on Generalized Embedding ⋮ Retrieving library functions by unifying types modulo linear isomorphism ⋮ Unification in sort theories and its applications ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Reduction of cycle unification of type \(Cpg+r\) ⋮ Unification in commutative semigroups ⋮ Constraints for polymorphic behaviours of concurrent ML ⋮ Set-term unification in a logic database language ⋮ Complete equational unification based on an extension of the Knuth-Bendix completion procedure ⋮ Unification in varieties of completely regular semigroups ⋮ Towards automated deduction in cP systems ⋮ Algebraic and logical aspects of unification ⋮ Model-theoretic aspects of unification ⋮ A modular order-sorted equational generalization algorithm ⋮ Unification in commutative rings is not finitary ⋮ Conditional equational theories and complete sets of transformations ⋮ Anti-unification and the theory of semirings ⋮ Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case ⋮ Extensions of unification modulo ACUI ⋮ Best solving modal equations ⋮ The unification hierarchy is undecidable ⋮ Combining matching algorithms: The regular case ⋮ What Is Essential Unification? ⋮ A compositional semantic basis for the analysis of equational Horn programs ⋮ A combinatory logic approach to higher-order E-unification ⋮ Discriminator varieties and symbolic computation ⋮ An order-sorted logic for knowledge representation systems ⋮ Unification in pseudo-linear sort theories is decidable ⋮ Unification theory ⋮ Hilbert's tenth problem is of unification type zero ⋮ Complexity of unification problems with associative-commutative operators ⋮ A new method for undecidability proofs of first order theories ⋮ Essential unifiers ⋮ Using types as search keys in function libraries ⋮ Order-sorted unification ⋮ Variadic equational matching in associative and commutative theories ⋮ Unnamed Item ⋮ A Modular Equational Generalization Algorithm ⋮ Unification and Passive Inference Rules for Modal Logics ⋮ A unification-theoretic method for investigating the \(k\)-provability problem ⋮ Category equivalence preserves unification type ⋮ A decision algorithm for distributive unification ⋮ Order-Sorted Generalization ⋮ Analogical projection in pattern perception ⋮ Unification in permutative equational theories is undecidable ⋮ Hyper tableaux ⋮ Termination of narrowing revisited ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV ⋮ Formalising nominal C-unification generalised with protected variables ⋮ Pattern-directed invocation with changing equations ⋮ Word unification and transformation of generalized equations ⋮ Unification in free distributive lattices ⋮ Termination by absence of infinite chains of dependency pairs

Uses Software

• MATHLAB
• REDUCE
• MACSYMA
• ALGOL 68
• SNOBOL

Cites Work

• Investigations in many-sorted quantor logic
• History and basic features of the critical-pair/completion procedure
• A Noetherian and confluent rewrite system for idempotent semigroups
• A fast string searching algorithm
• An improved proof procedure1
• Fast Decision Procedures Based on Congruence Closure
• Semantics-Based Translation Methods for Modal Logics
• An Algorithm for Subgraph Isomorphism
• Initial Algebra Semantics and Continuous Algebras
• The decision problem for equational bases of algebras
• The Concept of Demodulation in Theorem Proving
• Semi-Automated Mathematics
• Symbolic integration
• Resolution in type theory
• Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
• SNOBOL , A String Manipulation Language
• GIT—a heuristic program for testing pairs of directed line graphs for isomorphism
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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: Unification theory