Automatically assigned DDC number: 005131

Manually assigned DDC number: 005131

Title: Pumping, Cleaning and Symbolic Constraints Solving

Author:

Author:

Author:

Subject: Hubert Comon,Max Dauchet,Florent Jacquemard Pumping, Cleaning and Symbolic Constraints Solving

Description: We define a new class of tree automata which generalizes both the encompassment automata of [3] and the automata with tests between brothers of [2]. We give a pumping lemma for these automata, which implies that the emptiness of the corresponding language is decidable. Then, we show how to decide emptiness by means of a "cleaning" algorithm, which leads to more effective decision procedures. Introduction Ground reducibility of a term t with respect to a term rewriting system R is the property that all ground instances of t are reducible by R. This property is used in automatic proof by induction in equational theories [10, 1], in proving properties of equational specifications [11] and in constraint solving in quotient algebras [9]. Ground reducibility has been shown decidable in the general case by D. Plaisted [15], D. Kapur et al. [11], E. Kounalis [12]. Recently, some of us proved a more general result : the first order theory of encompassment is decidable [3]. More precisely, a t...

Contributor: The Pennsylvania State University CiteSeer Archives

Publisher: unknown

Date: 1995-04-19

Format: ps

Identifier: http://citeseer.ist.psu.edu/140262.html

Source: ftp://ftp.lifl.fr/pub/projects/LAC/ICALP94/icalp94-long.ps.Z

Language: en

Rights: unrestricted

Graph

<?xml   version="1.0"   encoding="UTF-8"?>

<references_metadata>

      <rec   ID="SELF"   Type="SELF"   CiteSeer_Book="SELF"   CiteSeer_Volume="SELF"   Title="Pumping,   Cleaning   and   Symbolic   Constraints   Solving">

            <identifier   Org="ISBN:0818679263"   Paper_ID="SELF"   Extracted="0818679263"   DDC="004"   Normalized_DDC="004"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:1402007493"   Paper_ID="SELF"   Extracted="1402007493"   DDC="530.13/8"   Normalized_DDC="530138"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540419500"   Paper_ID="SELF"   Extracted="3540419500"   DDC="005.1/1"   Normalized_DDC="00511"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540582010"   Paper_ID="SELF"   Extracted="3540582010"   />

            <identifier   Org="ISBN:354058403X"   Paper_ID="SELF"   Extracted="354058403X"   DDC="005.13/1"   Normalized_DDC="005131"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540592938"   Paper_ID="SELF"   Extracted="3540592938"   DDC="005.1"   Normalized_DDC="0051"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540593403"   Paper_ID="SELF"   Extracted="3540593403"   DDC="005.13/1"   Normalized_DDC="005131"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540615113"   Paper_ID="SELF"   Extracted="3540615113"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540627812"   Paper_ID="SELF"   Extracted="3540627812"   DDC="005.1/2"   Normalized_DDC="00512"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540647813"   Paper_ID="SELF"   Extracted="3540647813"   DDC="005.1"   Normalized_DDC="0051"   Normalized_Weight="0.1"   />

            <identifier   Org="ISBN:3540672575"   Paper_ID="SELF"   Extracted="3540672575"   DDC="005.1"   Normalized_DDC="0051"   Normalized_Weight="0.1"   />

      </rec>

</references_metadata>