Unification theory
From MaRDI portal
Publication:1124375
DOI10.1016/S0747-7171(89)80012-4zbMATH Open0678.68098OpenAlexW2914314632MaRDI QIDQ1124375FDOQ1124375
Authors: 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
Recommendations
Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- SNOBOL , A String Manipulation Language
- An Algorithm for Subgraph Isomorphism
- Title not available (Why is that?)
- Title not available (Why is that?)
- Initial Algebra Semantics and Continuous Algebras
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A fast string searching algorithm
- An improved proof procedure1
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
- Fast Decision Procedures Based on Congruence Closure
- Title not available (Why is that?)
- Resolution in type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Noetherian and confluent rewrite system for idempotent semigroups
- Title not available (Why is that?)
- Title not available (Why is that?)
- The decision problem for equational bases of algebras
- The Concept of Demodulation in Theorem Proving
- Title not available (Why is that?)
- Symbolic integration
- Title not available (Why is that?)
- Title not available (Why is that?)
- Investigations in many-sorted quantor logic
- Title not available (Why is that?)
- Semi-Automated Mathematics
- Title not available (Why is that?)
- History and basic features of the critical-pair/completion procedure
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- GIT—a heuristic program for testing pairs of directed line graphs for isomorphism
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Semantics-Based Translation Methods for Modal Logics
- Title not available (Why is that?)
Cited In (70)
- Reduction of cycle unification of type \(Cpg+r\)
- Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case
- An order-sorted logic for knowledge representation systems
- A Modular Equational Generalization Algorithm
- Hilbert's tenth problem is of unification type zero
- Anti-unification and the theory of semirings
- Incremental constraint satisfaction for equational logic programming
- Unification in commutative semigroups
- DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV
- Some results on equational unification
- Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification
- A new method for undecidability proofs of first order theories
- Complete equational unification based on an extension of the Knuth-Bendix completion procedure
- Unification and Passive Inference Rules for Modal Logics
- Word unification and transformation of generalized equations
- Unification theory
- A formalisation of nominal C-matching through unification with protected variables
- Unification, finite duality and projectivity in varieties of Heyting algebras
- Higher order E-unification
- Order-Sorted Generalization
- Title not available (Why is that?)
- Retrieving library identifiers via equational matching of types
- Termination of narrowing revisited
- Unification in partially commutative semigroups
- Order-sorted unification
- Termination by absence of infinite chains of dependency pairs
- Variadic equational matching in associative and commutative theories
- Discriminator varieties and symbolic computation
- An algorithm for distributive unification
- Complexity of unification problems with associative-commutative operators
- Best solving modal equations
- Combining matching algorithms: The regular case
- Undecidable properties of syntactic theories
- Generalizations of unification
- Unification in sort theories and its applications
- Retrieving library functions by unifying types modulo linear isomorphism
- Category equivalence preserves unification type
- Essential unifiers
- Unification in free distributive lattices
- Algebraic and logical aspects of unification
- Unification in permutative equational theories is undecidable
- Semi-unification of two terms in Abelian groups
- A decision algorithm for distributive unification
- The unification hierarchy is undecidable
- E-Unification based on Generalized Embedding
- Model-theoretic aspects of unification
- Unification in commutative rings is not finitary
- Conditional equational theories and complete sets of transformations
- Title not available (Why is that?)
- A modular order-sorted equational generalization algorithm
- Using types as search keys in function libraries
- Analogical projection in pattern perception
- Pattern-directed invocation with changing equations
- A unification-theoretic method for investigating the \(k\)-provability problem
- The Kreisel length-of-proof problem
- Unification in varieties of completely regular semigroups
- A formal semantics for DAI language NUML
- A compositional semantic basis for the analysis of equational Horn programs
- Hyper tableaux
- Set-term unification in a logic database language
- Linear and unit-resulting refutations for Horn theories
- A combinatory logic approach to higher-order E-unification
- Constraints for polymorphic behaviours of concurrent ML
- Title not available (Why is that?)
- Towards automated deduction in cP systems
- What Is Essential Unification?
- Unification in pseudo-linear sort theories is decidable
- Formalising nominal C-unification generalised with protected variables
- Extensions of unification modulo ACUI
- Implementation of a UU-algorithm for primitive recursive tree functions
Uses Software
This page was built for publication: Unification theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1124375)
