Unification in combinations of collapse-free regular theories

DOI10.1016/S0747-7171(87)80025-1zbMATH Open0638.68105OpenAlexW1968229471MaRDI QIDQ1099652FDOQ1099652

Katherine A. Yelick

Publication date: 1987

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(87)80025-1

Recommendations

• scientific article
• scientific article; zbMATH DE number 4049025
• scientific article; zbMATH DE number 4049130
• Unification in a combination of arbitrary disjoint equational theories
• Combining unification algorithms

zbMATH Keywords

reasoningassociative-commutative operatorscollapse-free regular theoriesequational unification algorithms

Mathematics Subject Classification ID

Equational logic, Mal'tsev conditions (08B05)

Cites Work

• A theory of type polymorphism in programming
• Simplification by Cooperating Decision Procedures
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An Efficient Unification Algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• Properties of substitutions and unifications
• Title not available (Why is that?)
• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• Title not available (Why is that?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Proofs by induction in equational theories with constructors
• Deciding Combinations of Theories
• 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?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• CLU reference manual
• REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies
• Oriented equational clauses as a programming language

Cited In (18)

• Unification algorithms cannot be combined in polynomial time.
• On equational theories, unification, and (un)decidability
• Unification theory
• Unification algorithms cannot be combined in polynomial time
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Terminating non-disjoint combined unification
• Unification in a combination of arbitrary disjoint equational theories
• Combining nonstably infinite theories
• Combining matching algorithms: The regular case
• Combining matching algorithms: The regular case
• Boolean unification - the story so far
• An overview of LP, the Larch Prover
• Modular higher-order E-unification
• Second-order unification in the presence of linear shallow algebraic equations
• On Asymmetric Unification and the Combination Problem in Disjoint Theories

Uses Software

• REVE

This page was built for publication: Unification in combinations of collapse-free regular theories

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