AUTOMATA FOR REDUCTION PROPERTIES SOLVING

Citation
M. Dauchet et al., AUTOMATA FOR REDUCTION PROPERTIES SOLVING, Journal of symbolic computation, 20(2), 1995, pp. 215-233
Citations number
14
Categorie Soggetti
Mathematics,"Computer Sciences, Special Topics",Mathematics,"Computer Science Theory & Methods
ISSN journal
07477171
Volume
20
Issue
2
Year of publication
1995
Pages
215 - 233
Database
ISI
SICI code
0747-7171(1995)20:2<215:AFRPS>2.0.ZU;2-2
Abstract
We introduce a new class of tree automata, which we call Reduction Aut omata (RA), and we use it to prove the decidability of the whole first order of theory of reduction (the theory of reduction is the set of t rue sentences built up with unary predicates red(t)(x) ''x is reducibl e by t'', i.e. ''some instance of t is a subterm of x''). So we link r ewriting, logic and formal languages.