6 Result(s)
within
Algorithm Analysis and Problem Complexity
Mathematical Logic and Formal Languages
Takahito Aoto
Chapter
Conference Paper
-
Chapter and Conference Paper
Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems
The notion of normal forms is ubiquitous in various equivalent transformations. Confluence (CR), one of the central properties of term rewriting systems (TRSs), concerns uniqueness of normal forms
-
Chapter and Conference Paper
Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems
Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet’s parallel closure theorem and its genera...
-
Chapter and Conference Paper
Termination of Rule-Based Calculi for Uniform Semi-Unification
Uniform semi-unification is a generalization of unification; its efficient algorithms have been extensively studied in (Kapur et al., 1994) and (Oliart&Snyder, 2004). For (uniform) semi-unification, several va...
-
Chapter and Conference Paper
Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering
In order to disprove confluence of term rewriting systems, we develop new criteria for ensuring non-joinability of terms based on interpretation and ordering. We present some instances of the criteria which ar...
-
Chapter and Conference Paper
Rational Term Rewriting Revisited: Decidability and Confluence
We consider a variant of rational term rewriting as first introduced by Corradini et al., i.e., we consider rewriting of (infinite) terms with a finite number of different subterms. Motivated by computability ...
-
Chapter and Conference Paper
Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
Simply typed term rewriting (Yamada, 2001) is a framework of higher-order term rewriting without bound variables based on Lisp-like syntax. The dependency pair method for the framework has been obtained by ext...
