Unification in the union of disjoint equational theories: Combining decision procedures
From MaRDI portal
Publication:1918503
DOI10.1006/jsco.1996.0009zbMath0851.68055OpenAlexW2082354652WikidataQ57383738 ScholiaQ57383738MaRDI QIDQ1918503
Publication date: 8 December 1996
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/451f9f9170c015e869a7d716fd6d8b35ae4217aa
Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (27)
Non-disjoint combined unification and closure by equational paramodulation ⋮ On the complexity of Boolean unification ⋮ Non-structural subtype entailment in automata theory ⋮ Model Checking Security Protocols ⋮ On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP ⋮ Rewriting modulo SMT and open system analysis ⋮ Equational unification, word unification, and 2nd-order equational unification ⋮ Verifying Cryptographic Protocols with Subterms Constraints ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Unification and Matching in Hierarchical Combinations of Syntactic Theories ⋮ Decidability and combination results for two notions of knowledge in security protocols ⋮ \(E\)-unification with constants vs. general \(E\)-unification ⋮ Extensions of unification modulo ACUI ⋮ Solving equations with sequence variables and sequence functions ⋮ Symbolic protocol analysis for monoidal equational theories ⋮ Hierarchical combination of intruder theories ⋮ Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures ⋮ Combinable Extensions of Abelian Groups ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ A Proof Theoretic Analysis of Intruder Theories ⋮ Unification modulo lists with reverse relation with certain word equations ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Unification algorithms cannot be combined in polynomial time. ⋮ Solvability of context equations with two context variables is decidable ⋮ Formalising nominal C-unification generalised with protected variables ⋮ Terminating non-disjoint combined unification
This page was built for publication: Unification in the union of disjoint equational theories: Combining decision procedures
