What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
AC-unifier algebra algorithm alien subterms applied arbitrary assume binary function symbol Boolean Boolean rings Buchberger's algorithm C-unification coefficient collapsing computation confluent congruence closure contains critical pairs decidable decision procedure defined definition denote E-algebra elements equational theory equivalent example Exercise exists finite set free algebra function symbols functional programming ground terms halting problem hence holds homomorphism idempotent implementation implies induction infinite joinable Knuth-Bendix order left-linear Lemma lexicographic path order linear minimal complete set modulo monomial multiset nodes nontrivial normal form obtained occurs check orthogonal partial order proof prove recursive reduction order relation rewrite rule satisfies set of identities set of variables signature simplification order Sj-i solution step strict order substitution term rewriting system termination Theorem trivial Turing machine unary function undecidable unification problem unifier Var(t well-founded word problem yields
From other books
All Book Search results »
From Google Scholar
Stephan Schulz - 2002 - AI Communications
Gilles Dowek, Thérèse Hardin, Claude Kirchner - 2003 - Journal of Automated Reasoning
Christoph Weidenbach - 2001
All Scholar search results »
HORATIU CIRSTEA, CLAUDE KIRCHNER - Logic Journal of IGPL
Term rewriting and all that - Software, IEE Proceedings- [see also ...
Term Rewriting and All That by Franz Baader and Tobias Nipkow ...
concurrency: llelism The Optimal Implementation of tmctional ...
Term Rewriting and All That
Confluence (term rewriting) - Wikipedia, the free encyclopedia
Term rewriting system for code generation, and its termination ...
JSTOR: Term Rewriting Systems
Descendants and Origins in Term Rewriting (researchindex)
Theory and Practice of Formal Proofs