Decidable Fragments of Simultaneous Rigid Reachability (1999)  (Make Corrections)  (2 citations)
Veronique Cortier, Harald Ganziger, Florent Jacquemard, Margus Veanes
Lecture Notes in Computer Science

  Home/Search   Context   Related

Links:   ACM   DBLP

 
View or download:
mpisb.mpg.de/~hg/paper...99ICALP.ps.gz
Cached:  PS.gz  PS  PDF  Image  Update  Help

From:  mpisb.mpg.de/~hg/pap...abstracts (more)
(Enter author homepages)

Rate this article: (best)
  Comment on this article  
(Enter summary)

Abstract: In this paper we prove decidability results of restricted fragments of simultaneous rigid reachability or SRR, that is the nonsymmetrical form of simultaneous rigid E-unification or SREU. The absence of symmetry enforces us to use different methods, than the ones that have been successful in the context of SREU (for example word equations). The methods that we use instead, involve finite (tree) automata techniques, and the decidability proofs provide precise computational complexity bounds. The ... (Update)

Context of citations to this paper:   More

...The authors wish to thank the referees for their useful remarks and suggestions, which led to signi cant improvements of the results. The PSPACE upper bound of monadic SRR with ground rules has been obtained by joint work with Veronique Cortier, and was published in...

.... interested in ground solutions, i.e. in solutions such that x ; y ; z More results appeared in later papers, for example [69,63,64,71,10,70,27,9,65,35,72] [73,32,48,61] Veanes produced a series of very transparent proofs of stronger results [63,64] based on the techniques by...

Cited by:   More
Herbrand's Theorem And Equational Reasoning: Problems.. - Degtyarev, Gurevich.. (1996)   (Correct)
Rigid Reachability The Non-Symmetric Form Of Rigid E-Unification - Ganzinger (2000)   (Correct)

Active bibliography (related documents):   More   All
0.4:   Tree Automata Techniques and Applications -.. - Comon, Dauchet..   (Correct)
0.4:   Tree Automata Techniques and Applications -.. - Comon, Dauchet.. (1998)   (Correct)
0.4:   Tree Automata Techniques and Applications -.. - Comon, Dauchet..   (Correct)

Similar documents based on text:   More   All
1.3:   Decidability and Complexity of Simultaneous Rigid.. - Degtyarev.. (1997)   (Correct)
0.4:   Rigid Reachability - Ganzinger, Jacquemard, Veanes (1998)   (Correct)
0.4:   Unification in Extensions of Shallow Equational Theories - Jacquemard, Meyer, Weidenbach (1998)   (Correct)

Related documents from co-citation:   More   All
2:   The decidability of simultaneous rigid E-unication with one variable (context) - Degtyarev, Gurevich et al.

BibTeX entry:   (Update)

V. Cortier, H. Ganzinger, F. Jacquemard, and M. Veanes. Decidable fragments of simultaneous rigid reachability. In Proc. 26th Int. Coll. on Automata, Languages and Programming, ICALP99, Prague, volume 1644 of Lecture Notes in Computer Science. Springer-Verlag, july 1999. http://citeseer.ist.psu.edu/cortier99decidable.html   More

@article{ cortier99decidable,
    author = "Veronique Cortier and Harald Ganzinger and Florent Jacquemard and Margus Veanes",
    title = "Decidable Fragments of Simultaneous Rigid Reachability",
    journal = "Lecture Notes in Computer Science",
    volume = "1644",
    pages = "250--??",
    year = "1999",
    url = "citeseer.ist.psu.edu/cortier99decidable.html" }
Citations (may not include all citations):
102   Tree acceptors and some of their applications (context) - Doner - 1970  DBLP
96   Tree Automata Techniques and Applications - Comon, Dauchet et al. - 1998
52   Lower bounds for natural proof systems (context) - Kozen - 1977  DBLP
33   Alternation (context) - Chandra, Kozen et al. - 1981  ACM   DBLP
30   Generalized nite automata theory with an application to a de.. (context) - Thatcher, Wright - 1968
19   Rewriting and tree automata (context) - Dauchet - 1993  ACM   DBLP
13   Makanin's algorithm: Two improvements and a generalization (context) - Schulz - 1990
10   The decidability of simultaneous rigid E-unication with one .. (context) - Degtyarev, Gurevich et al.
10   Rigid reachability - Ganzinger, Jacquemard et al. - 1998  ACM   DBLP
10   Bottom-up tree pushdown automata: classication and connectio.. (context) - Dauchet, Gilleron et al. - 1994
9   Theorem proving using rigid E-unication: Equational matings (context) - Gallier, Raatz et al. - 1987
7   Decidability of the con- uence of nite ground term rewrite s.. (context) - Dauchet, Heuillard et al. - 1990
4   Decidable and undecidable second-order unication problems (context) - Levy - 1998
4   Simple second-order languages for which unication is undecid.. (context) - Farmer - 1991
2   unication is NP-complete (context) - Gallier, Narendran et al. - 1988
2   The relation between second-order unication and simultaneous.. (context) - Veanes - 1998
1   Simultaneous rigid E- unication and related algorithmic prob.. (context) - Degtyarev, Matiyasevich et al. - 1996
1   Simultaneous rigid E-unication and other decision problems r.. (context) - Voronkov - 1998

Documents on the same site (http://www.mpi-sb.mpg.de/~hg/papers/conferences/abstracts.html):   More
A Resolution-Based Decision Procedure for Extensions of K4 - Ganzinger, Hustadt.. (1998)   (Correct)
Soft Typing for Ordered Resolution - Ganzinger, Meyer, Weidenbach (1996)   (Correct)
Complexity Analysis Based on Ordered Resolution - Basin, Ganzinger (1996)   (Correct)

Online articles have much greater impact   More about CiteSeer.IST   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST - Copyright Penn State and NEC