scientific article

zbMath0516.68067MaRDI QIDQ3664457

Claude Kirchner, Jean-Pierre Jouannaud, Hélène Kirchner

Publication date: 1983

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

automatic theorem provingunification problemequational term rewriting systemincremental waynoetherian term rewriting systemsigned binary trees theory

Mathematics Subject Classification ID

Related Items (25)

Unification in combinations of collapse-free regular theories ⋮ A class of confluent term rewriting systems and unification ⋮ Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties ⋮ History and basic features of the critical-pair/completion procedure ⋮ Complete symbolic reachability analysis using back-and-forth narrowing ⋮ Unnamed Item ⋮ Enumerating outer narrowing derivations for constructor-based term rewriting systems ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ Twenty years of rewriting logic ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Effectively Checking the Finite Variant Property ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs ⋮ Narrowing based procedures for equational disunification ⋮ Variant Narrowing and Equational Unification ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Programming and symbolic computation in Maude ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Conditional narrowing modulo a set of equations ⋮ Schematization of infinite sets of rewrite rules generated by divergent completion processes ⋮ Complete sets of unifiers and matchers in equational theories ⋮ Narrowing and Rewriting Logic: from Foundations to Applications ⋮ Symbolic computation in Maude: some tapas

This page was built for publication: