A unified view of tree automata and term schematisations

Abstract

We propose an extension of tree automata, called N-automata, which captures some of the features of term schematisation languages, for instance the use of counter variables and parameters. We show that the satisfiability problem is decidable for positive, purely existential, membership formulae which permits to include the proposed formalism into most existing symbolic computation procedures (such as SLD-resolution). © 2008 Springer Science+Business Media, LLC.