24 Result(s)
within
English
Takahito Aoto
Chapter
-
Chapter and Conference Paper
A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
The rewrite relation of a conditional term rewriting system (CTRS) can be divided into a hierarchy of rewrite relations of term rewriting systems (TRSs) by the depth of the recursive use of rewrite relation in...
-
Chapter and Conference Paper
Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables
Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. Recently, a new format of nominal rewriting has been introduced where rewrit...
-
Chapter and Conference Paper
Commutative Rational Term Rewriting
Term rewriting for rational terms, i.e. infinite terms with a finite number of different subterms, has been considered e.g. in Corradini & Gadducci (1998) and Aoto & Ketema (2012). In this paper, we consider r...
-
Chapter and Conference Paper
A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. In this paper, we present a proof method for local sufficient completeness of TRSs, which i...
-
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
Ultra-Shallow DoF Imaging Using Faced Paraboloidal Mirrors
We propose a new imaging method that achieves an ultra-shallow depth of field (DoF) to clearly visualize a particular depth in a 3-D scene. The key optical device consists of a pair of faced paraboloidal mirro...
-
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
Nominal Confluence Tool
Nominal rewriting is a framework of higher-order rewriting introduced in (Fernández, Gabbay & Mackie, 2004; Fernández & Gabbay, 2007). Recently, (Suzuki et al., 2015) revisited confluence of nominal rewriting ...
-
Chapter and Conference Paper
Confluence Competition 2015
Confluence is one of the central properties of rewriting. Our competition aims to foster the development of techniques for proving/disproving confluence of various formalisms of rewriting automatically. We exp...
-
Chapter and Conference Paper
Correctness of Context-Moving Transformations for Term Rewriting Systems
Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for fu...
-
Chapter and Conference Paper
Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams
The decreasing diagrams technique (van Oostrom, 1994) has been successfully used to prove confluence of rewrite systems in various ways; using rule-labelling (van Oostrom, 2008), it can also be applied directl...
-
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
Proving Confluence of Term Rewriting Systems Automatically
We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our pro...
-
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...
-
Chapter and Conference Paper
RAPT: A Program Transformation System Based on Term Rewriting
Chiba et al. (2005) proposed a framework of program transformation by template based on term rewriting in which correctness of the transformation is verified automatically. This paper describes RAPT (Rewriting-ba...
-
Chapter and Conference Paper
Dealing with Non-orientable Equations in Rewriting Induction
Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction orde...
-
Chapter and Conference Paper
Dependency Pairs for Simply Typed Term Rewriting
Simply typed term rewriting proposed by Yamada (RTA, 2001) is a framework of higher-order term rewriting without bound variables. In this paper, the dependency pair method of first-order term rewriting introdu...
-
Chapter and Conference Paper
Inductive Theorems for Higher-Order Rewriting
Based on the simply typed term rewriting framework, inductive reasoning in higher-order rewriting is studied. The notion of higher-order inductive theorems is introduced to reflect higher-order feature of simp...
