Rigid reachability

Ganzinger, Harald; Jacquemard, Florent; Veanes, Margus

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

このアイテムの新しいバージョンが利用可能です:
https://pure.mpg.de/pubman/item/item_1819396_4

詳細要約

公開

報告書

Rigid reachability

MPS-Authors

/persons/resource/persons44474

Ganzinger, Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44688

Jacquemard, Florent
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45662

Veanes, Margus
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

1998-2-013
(全文テキスト（全般）), 10KB

付随資料 (公開)

There is no public supplementary material available

引用

Ganzinger, H., Jacquemard, F., & Veanes, M.(1998). Rigid reachability (MPI-I-1998-2-013). Saarbrücken: Max-Planck-Institut für Informatik.

引用: https://hdl.handle.net/11858/00-001M-0000-0014-768F-9

要旨

We show that rigid reachability, the non-symmetric form of rigid E-unification, is undecidable already in the case of a single constraint. From this we infer the undecidability of a new rather restricted kind of second-order unification. We also show that certain decidable subclasses of the problem which are PTIME-complete in the equational case become EXPTIME-complete when symmetry is absent. By applying automata-theoretic methods, simultaneous monadic rigid reachability with ground rules is shown to be in EXPTIME.