Unification in combinations of collapse-free regular theories
From MaRDI portal
Publication:1099652
Recommendations
Cites work
- scientific article; zbMATH DE number 3885353 (Why is no real title available?)
- scientific article; zbMATH DE number 3867289 (Why is no real title available?)
- scientific article; zbMATH DE number 3871322 (Why is no real title available?)
- scientific article; zbMATH DE number 3871334 (Why is no real title available?)
- scientific article; zbMATH DE number 3817070 (Why is no real title available?)
- scientific article; zbMATH DE number 3829296 (Why is no real title available?)
- scientific article; zbMATH DE number 3896335 (Why is no real title available?)
- scientific article; zbMATH DE number 3936507 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3466489 (Why is no real title available?)
- scientific article; zbMATH DE number 3227055 (Why is no real title available?)
- scientific article; zbMATH DE number 3290336 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- scientific article; zbMATH DE number 3019695 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A Unification Algorithm for Associative-Commutative Functions
- A theory of type polymorphism in programming
- An Efficient Unification Algorithm
- CLU reference manual
- Complete Sets of Reductions for Some Equational Theories
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Deciding Combinations of Theories
- Oriented equational clauses as a programming language
- Proofs by induction in equational theories with constructors
- Properties of substitutions and unifications
- REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies
- Simplification by Cooperating Decision Procedures
Cited in
(18)- On equational theories, unification, and (un)decidability
- Boolean unification - the story so far
- Combining matching algorithms: The regular case
- Unification algorithms cannot be combined in polynomial time
- Combining nonstably infinite theories
- Modular higher-order E-unification
- Combining matching algorithms: The regular case
- scientific article; zbMATH DE number 3945372 (Why is no real title available?)
- On Asymmetric Unification and the Combination Problem in Disjoint Theories
- scientific article; zbMATH DE number 4049025 (Why is no real title available?)
- scientific article; zbMATH DE number 4049130 (Why is no real title available?)
- scientific article; zbMATH DE number 4112560 (Why is no real title available?)
- An overview of LP, the Larch Prover
- Unification algorithms cannot be combined in polynomial time.
- Unification theory
- Terminating non-disjoint combined unification
- Second-order unification in the presence of linear shallow algebraic equations
- Unification in a combination of arbitrary disjoint equational theories
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)
