scientific article

zbMath0441.68108MaRDI QIDQ3883561

Jean-Marie Hullot

Publication date: 1980

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

zbMATH Keywords

unificationequational theoriescanonical term rewriting systemsFay's algorithmnarrowing process

Mathematics Subject Classification ID

Related Items (only showing first 100 items - show all)

A new approach to general E-unification based on conditional rewriting systems ⋮ An optimal narrowing strategy for general canonical systems ⋮ Relative termination via dependency pairs ⋮ Towards Erlang Verification by Term Rewriting ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ Completion-time optimization of rewrite-time goal solving ⋮ Narrowing and unification in functional programming —An evaluation mechanism for absolute set abstraction ⋮ Negation with logical variables in conditional rewriting ⋮ Rewriting, and equational unification: the higher-order cases ⋮ Detecting redundant narrowing derivations by the LSE-SL reducibility test ⋮ Narrowing directed by a graph of terms ⋮ Incremental techniques for efficient normalization of nonlinear rewrite systems ⋮ Improving transformation systems for general E-unification ⋮ On narrowing, refutation proofs and constraints ⋮ Implementation of a UU-algorithm for primitive recursive tree functions ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ Termination of rewriting ⋮ Unification problems with one-sided distributivity ⋮ Unification in combinations of collapse-free regular theories ⋮ Simplifying conditional term rewriting systems: Unification, termination and confluence ⋮ A class of confluent term rewriting systems and unification ⋮ Kernel-LEAF: A logic plus functional language ⋮ Unification modulo an equality theory for equational logic programming ⋮ History and basic features of the critical-pair/completion procedure ⋮ Narrowing vs. SLD-resolution ⋮ Complete symbolic reachability analysis using back-and-forth narrowing ⋮ A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Incremental constraint satisfaction for equational logic programming ⋮ Infinite complete group presentations ⋮ Enumerating outer narrowing derivations for constructor-based term rewriting systems ⋮ An integrated framework for the diagnosis and correction of rule-based programs ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ A new generic scheme for functional logic programming with constraints ⋮ Axiomatization of a functional logic language ⋮ Equation solving in conditional AC-theories ⋮ Optimization of rewriting and complexity of rewriting ⋮ On modularity in term rewriting and narrowing ⋮ An introduction to category-based equational logic ⋮ Lazy narrowing: Strong completeness and eager variable elimination (extended abstract) ⋮ A framework for incremental learning of logic programs ⋮ The unification problem for confluent right-ground term rewriting systems. ⋮ Modular Termination of Basic Narrowing ⋮ A modular order-sorted equational generalization algorithm ⋮ On completeness of narrowing strategies ⋮ On ground-confluence of term rewriting systems ⋮ A rationale for conditional equational programming ⋮ Conditional equational theories and complete sets of transformations ⋮ A Noetherian and confluent rewrite system for idempotent semigroups ⋮ Unnamed Item ⋮ Theorem proving modulo ⋮ Proving convergence of self-stabilizing systems using first-order rewriting and regular languages ⋮ Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ A rewrite-based type discipline for a subset of computer algebra ⋮ Completion for unification ⋮ Specification and proof in membership equational logic ⋮ Termination of term rewriting using dependency pairs ⋮ A typed functional extension of logic programming ⋮ A compositional semantic basis for the analysis of equational Horn programs ⋮ Lazy narrowing: strong completeness and eager variable elimination ⋮ Unification and matching modulo nilpotence ⋮ Narrowing based procedures for equational disunification ⋮ Proof normalization modulo ⋮ An improved general \(E\)-unification method ⋮ C-expressions: A variable-free calculus for equational logic programming ⋮ Well rewrite orderings and well quasi-orderings ⋮ Programming with narrowing: a tutorial ⋮ Termination of narrowing via termination of rewriting ⋮ Variant Narrowing and Equational Unification ⋮ A compact fixpoint semantics for term rewriting systems ⋮ Unification in Boolean rings and Abelian groups ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Constant runtime complexity of term rewriting is semi-decidable ⋮ Termination of Narrowing in Left-Linear Constructor Systems ⋮ Key Substitution in the Symbolic Analysis of Cryptographic Protocols ⋮ On the connection between narrowing and proof by consistency ⋮ Decidable higher-order unification problems ⋮ Conditional narrowing modulo a set of equations ⋮ Complete sets of transformations for general E-unification ⋮ Synthesis of rewrite programs by higher-order and semantic unification ⋮ A strong restriction of the inductive completion procedure ⋮ Horn equational theories and paramodulation ⋮ Basic narrowing revisited ⋮ On equational theories, unification, and (un)decidability ⋮ Unification in permutative equational theories is undecidable ⋮ Termination of narrowing revisited ⋮ Conditions for confluence of innermost terminating term rewriting systems ⋮ A hybrid programming scheme combining fuzzy-logic and functional-logic resources ⋮ Higher order unification via explicit substitutions ⋮ Complexity of nilpotent unification and matching problems. ⋮ Automata-driven automated induction ⋮ A Non-Deterministic Multiset Query Language ⋮ Refutational theorem proving using term-rewriting systems ⋮ Equational methods in first order predicate calculus ⋮ Narrowing and Rewriting Logic: from Foundations to Applications ⋮ Termination by absence of infinite chains of dependency pairs ⋮ Symbolic computation in Maude: some tapas

This page was built for publication: