Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator

Nicolini E., Ringeissen C., Rusinowitch M.

Fundamenta Informaticae

2011

Vol. 105, nr 1/2

163-187

We present some decidability results for the universal fragment of theories modeling data structures and endowed with arithmetic constraints. More precisely, all the theories taken into account extend a theory that constrains the function symbol for the successor. A general decision procedure is obtained, by devising an appropriate calculus based on superposition. Moreover, we derive a decidability result for the combination of the considered theories for data structures and some fragments of arithmetic by applying a general combination schema for theories sharing a common subtheory. The effectiveness of the resulting algorithm is ensured by using the proposed calculus and a careful adaptation of standard methods for reasoning about arithmetic, such as Gauss elimination, Fourier-Motzkin elimination and Groebner bases computation.

Algorithms and reductions for rewriting problems

Verma R.M., Rusinowitch M., Lugiez D.

Fundamenta Informaticae

2001

Vol. 46, nr 3

257-276

In this paper we initiate a study of polynomial-time reductions for some basic decision problems of rewrite systems. We then give a polynomial-time algorithm for the unique-normal-form property of ground systems for the first time. Next we prove undecidability of several problems for a fixed string rewriting system using our reductions. Finally, we prove the decidability of confluence for commutative semi-thue systems. The Confluence and Unique-normal-form property are shown Expspace-hard for commutative semi-thue systems. We also show that there is a family of string rewrite systems for which the word problem is trivially decidable but confluence is undecidable, and we show a linear equational theory with decidable word problem but undecidable linear equational matching problem.