scientific article; zbMATH DE number 3413831
From MaRDI portal
Publication:5678447
zbMath0262.68036MaRDI QIDQ5678447
Publication date: 1972
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Unification in varieties of completely regular semigroups ⋮ Makanin's algorithm for word equations-two improvements and a generalization ⋮ Strategies in conditional narrowing modulo SMT plus axioms ⋮ Unification theory ⋮ A resolution principle for constrained logics ⋮ Constrained equational deduction ⋮ On solving the equality problem in theories defined by Horn clauses ⋮ Automated deduction with associative-commutative operators ⋮ Alternating two-way AC-tree automata ⋮ On unification: Equational theories are not bounded ⋮ Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent ⋮ CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems ⋮ Characterizations of unification type zero ⋮ Rewriting, and equational unification: the higher-order cases ⋮ Formal parametric equations ⋮ A note on unification type zero ⋮ Complexity of matching problems ⋮ Associative-commutative unification ⋮ Unification in combinations of collapse-free regular theories ⋮ Embedding Boolean expressions into logic programming ⋮ A class of confluent term rewriting systems and unification ⋮ Unification modulo an equality theory for equational logic programming ⋮ History and basic features of the critical-pair/completion procedure ⋮ Computers and universal algebra: Some directions ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Unification in commutative idempotent monoids ⋮ Finite generation of ambiguity in context-free languages ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ On Skolemization in constrained logics ⋮ Enumerating outer narrowing derivations for constructor-based term rewriting systems ⋮ Makanin's algorithm is not primitive recursive ⋮ Unnecessary inferences in associative-commutative completion procedures ⋮ On First-Order Model-Based Reasoning ⋮ Multi-modal logic programming using equational and order-sorted logic ⋮ Unification properties of commutative theories: A categorical treatment ⋮ Unification of infinite sets of terms schematized by primal grammars ⋮ When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus ⋮ Projectivity and unification in substructural logics of generalized rotations ⋮ Towards parametrizing word equations ⋮ The complexity of counting problems in equational matching ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Unification in commutative rings is not finitary ⋮ Conditional equational theories and complete sets of transformations ⋮ Rigid E-unification: NP-completeness and applications to equational matings ⋮ Theorem proving modulo ⋮ Superposition with completely built-in abelian groups ⋮ Completion for unification ⋮ Solving equations with sequence variables and sequence functions ⋮ The unification hierarchy is undecidable ⋮ Learning elementary formal systems ⋮ What Is Essential Unification? ⋮ T-string unification: Unifying prefixes in non-classical proof methods ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ Unification algorithms cannot be combined in polynomial time ⋮ Unification and matching modulo nilpotence ⋮ Path indexing for AC-theories ⋮ Proof normalization modulo ⋮ Multimodal logic programming using equational and order-sorted logic ⋮ Complexity of unification problems with associative-commutative operators ⋮ An improved general \(E\)-unification method ⋮ Order-sorted Equational Unification Revisited ⋮ Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically ⋮ A new method for undecidability proofs of first order theories ⋮ Anti-patterns for rule-based languages ⋮ Essential unifiers ⋮ Combinable Extensions of Abelian Groups ⋮ Unification in commutative theories ⋮ Unification in Boolean rings and Abelian groups ⋮ Order-sorted unification ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Non-resolution theorem proving ⋮ Solving word equations ⋮ Flat matching ⋮ Towards the automation of set theory and its logic ⋮ Associative-commutative deduction with constraints ⋮ Completion for rewriting modulo a congruence ⋮ Complete sets of transformations for general E-unification ⋮ Symbolic constraint handling through unification in finite algebras ⋮ Theorem-proving with resolution and superposition ⋮ On word problems in Horn theories ⋮ Complete sets of unifiers and matchers in equational theories ⋮ Identity Problems, Solvability of Equations and Unification in Varieties of Semigroups Related to Varieties of Groups ⋮ Tactics for Reasoning Modulo AC in Coq ⋮ The structure-mapping engine: Algorithm and examples ⋮ Horn equational theories and paramodulation ⋮ Unification problem in equational theories ⋮ On equational theories, unification, and (un)decidability ⋮ On equality up-to constraints over finite trees, context unification, and one-step rewriting ⋮ A practical integration of first-order reasoning and decision procedures ⋮ Swinging types=functions+relations+transition systems ⋮ Higher order unification via explicit substitutions ⋮ Complexity of nilpotent unification and matching problems. ⋮ Unification algorithms cannot be combined in polynomial time. ⋮ E-matching for Fun and Profit ⋮ Refutational theorem proving using term-rewriting systems ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Subset-equational programming in intelligent decision systems ⋮ Equational methods in first order predicate calculus ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Word unification and transformation of generalized equations ⋮ Competing for the \(AC\)-unification race ⋮ Properties of substitutions and unifications ⋮ Symbolic computation in Maude: some tapas
