A Terminating and Confluent Term Rewriting System for the Pure Equational Theory of Quandles

2018 ◽  
Author(s):  
Robert W. McGrail ◽  
Thuy Trang Nguyen ◽  
Thanh Thuy Trang Tran ◽  
Arti Tripathi
Keyword(s):  
Equational Theory ◽  
Term Rewriting ◽  
Term Rewriting System ◽  
Rewriting System

scholarly journals IDENTITIES IN THE ALGEBRA OF PARTIAL MAPS

2006 ◽  
Vol 16 (06) ◽  
pp. 1131-1159 ◽  
Author(s):  
MARCEL JACKSON ◽  
TIM STOKES
Keyword(s):  
Word Problem ◽  
Equational Theory ◽  
Term Rewriting ◽  
Deductive System ◽  
Natural Order ◽  
Term Rewriting System ◽  
Rewriting System ◽  
Clifford Semigroups

We consider the identities of a variety of semigroup-related algebras modelling the algebra of partial maps. We show that the identities are intimately related to a weak semigroup deductive system and we show that the equational theory is decidable. We do this by giving a term rewriting system for the variety. We then show that this variety has many subvarieties whose equational theory interprets the full uniform word problem for semigroups and consequently are undecidable. As a corollary it is shown that the equational theory of Clifford semigroups whose natural order is a semilattice is undecidable.

LEARNING FROM EXAMPLES IN UNIVERSE OF DISCOURSE DESCRIBED BY A SET OF EQUATIONS

1992 ◽  
Vol 01 (03) ◽  
pp. 333-350
Author(s):  
EMMANUEL KOUNALIS
Keyword(s):  
Background Knowledge ◽  
Term Rewriting ◽  
Learning From Examples ◽  
Implicit Representation ◽  
Term Rewriting System ◽  
Rewriting System ◽  
Finite Set ◽  
Formal Basis ◽  
Knowledge Problem ◽  
Universe Of Discourse

Generalization is an important operation for programs that learn. Anti-unification guarantees the existence of a term which is the most specific generalization of a collection of terms. This provides a formal basis for learning from examples. However, such generalization may be "too" general and therefore counterexamples are required to restrict them. In this case, the learner has to check whether the resulting formula provides a concept to learn, i.e. whether a formula of the form t/{t1,…,tn} is a generalization, where t is viewed as a generalization of a set of examples and t1,…,tn are counterexample. The formula t/{t1,…,tn} is often called an implicit representation. The implicit representation t/{t1,…,tn} is a generalization iff there exist ground (variable-free) instances of t which are not instances of t1,…,tn. This is a non-trivial task even when there is no background knowledge (see [15]). We present here a method to check whether an implicit representation t/{t1,…,tn} is a generalization with respect to a finite set of equations which describes the background knowledge problem, i.e. whether there exists a ground instance of t which is not equivalent to any ground instance of t1,…,tn with respect to a set E of equations. Whereas this problem is in general undecidable since the equality is so, we show in this paper that in this case where the set E of equations is compiled into a ground convergent term rewriting system, we can discover concepts in Universe of Discourse with background knowledge described by a finite set of equations. We show how the method applies to induce concepts in theories of elementary arithmetic.

scholarly journals HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA

2009 ◽  
Vol 20 (05) ◽  
pp. 837-849 ◽  
Author(s):  
YOHAN BOICHUT ◽  
ROMEO COURBIS ◽  
PIERRE-CYRILLE HEAM ◽  
OLGA KOUCHNARENKO
Keyword(s):  
General Problem ◽  
Transitive Closure ◽  
Term Rewriting ◽  
Tree Automata ◽  
Regular Model ◽  
Term Rewriting System ◽  
Rewriting System ◽  
Regular Model Checking ◽  
Successor Relation ◽  
Tree Languages

This paper addresses the following general problem of tree regular model-checking: decide whether [Formula: see text] where [Formula: see text] is the reflexive and transitive closure of a successor relation induced by a term rewriting system [Formula: see text], and [Formula: see text] and [Formula: see text] are both regular tree languages. We develop an automatic approximation-based technique to handle this – undecidable in general – problem in the case when term rewriting system rules are non left-linear.

scholarly journals Calculation of Fundamental Groups via Computational Paths

2021 ◽  
Author(s):  
T. M. L. de Veras ◽  
A. F. Ramos ◽  
R. J. G. B. de Queiroz ◽  
A. G. de Oliveira
Keyword(s):  
Projective Plane ◽  
Term Rewriting ◽  
Fundamental Groups ◽  
Real Projective Plane ◽  
The Real ◽  
Term Rewriting System ◽  
Rewriting System

We address the question as to how to formalise the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. The intention is to demonstrate the use of a term rewriting system in performing computations with these computational paths, establishing equalities between equalities, and further higher equalities, in particular, in the calculation of fundamental groups of surfaces such as the circle, the torus and the real projective plane.

Sign in / Sign up

Export Citation Format

Share Document