scientific article; zbMATH DE number 3413831

Cited in

(only showing first 100 items - show all)

Equational methods in first order predicate calculus
Properties of substitutions and unifications
On solving the equality problem in theories defined by Horn clauses
On unification: Equational theories are not bounded
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
History and basic features of the critical-pair/completion procedure
Unification in commutative idempotent monoids
Finite generation of ambiguity in context-free languages
Enumerating outer narrowing derivations for constructor-based term rewriting systems
Makanin's algorithm is not primitive recursive
Completion for unification
The unification hierarchy is undecidable
Learning elementary formal systems
Multimodal logic programming using equational and order-sorted logic
An improved general \(E\)-unification method
A new method for undecidability proofs of first order theories
Non-resolution theorem proving
Towards the automation of set theory and its logic
Completion for rewriting modulo a congruence
Complete sets of transformations for general E-unification
Unification problem in equational theories
Word unification and transformation of generalized equations
Competing for the \(AC\)-unification race
A resolution principle for constrained logics
Automated deduction with associative-commutative operators
On Skolemization in constrained logics
Unification of infinite sets of terms schematized by primal grammars
Theorem proving modulo
Superposition with completely built-in abelian groups
Swinging types=functions+relations+transition systems
Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
Complete sets of unifiers and matchers in equational theories
The structure-mapping engine: Algorithm and examples
Horn equational theories and paramodulation
On equational theories, unification, and (un)decidability
Higher order unification via explicit substitutions
Complexity of nilpotent unification and matching problems.
Unification algorithms cannot be combined in polynomial time.
Cancellative Abelian monoids and related structures in refutational theorem proving. I
Computers and universal algebra: Some directions
Combination problems for commutative/monoidal theories or how algebra can help in equational unification
Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Symbolic computation in Maude: some tapas
First-order automated reasoning with theories: when deduction modulo theory meets practice
Alternating two-way AC-tree automata
Solving equations with sequence variables and sequence functions
Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
Essential unifiers
Unification modulo an equality theory for equational logic programming
Projectivity and unification in substructural logics of generalized rotations
E-matching for fun and profit
On First-Order Model-Based Reasoning
Identity problems, solvability of equations and unification in varieties of semigroups related to varieties of groups
Tactics for Reasoning Modulo AC in Coq
What is essential unification?
Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent
CoLL: a confluence tool for left-linear term rewrite systems
Unnecessary inferences in associative-commutative completion procedures
Towards parametrizing word equations
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
Characterizations of unification type zero
Rewriting, and equational unification: the higher-order cases
Formal parametric equations
Multi-modal logic programming using equational and order-sorted logic
Unification properties of commutative theories: a categorical treatment
Order-sorted equational unification revisited
Combinable Extensions of Abelian Groups
Associative-commutative deduction with constraints
The complexity of counting problems in equational matching
On equality up-to constraints over finite trees, context unification, and one-step rewriting
A practical integration of first-order reasoning and decision procedures
Unification in commutative theories
Unification in Boolean rings and Abelian groups
Order-sorted unification
Unification in a combination of arbitrary disjoint equational theories
Constrained equational deduction
Solving word equations
When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
Unification in varieties of completely regular semigroups
Makanin's algorithm for word equations-two improvements and a generalization
Unification theory
Strategies in conditional narrowing modulo SMT plus axioms
scientific article; zbMATH DE number 7680806 (Why is no real title available?)
An improved general E-unification method
Rewrite systems for varieties of semigroups
Higher order E-unification
Positive deduction modulo regular theories
Confluence of conditional rewriting modulo
Complexity of unification problems with associative-commutative operators
Canonical for automated theorem proving in Lean

This page was built for publication:

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