A note on Presburger arithmetic with array segments, permutation and equality (Q1073009): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 03:06, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A note on Presburger arithmetic with array segments, permutation and equality |
scientific article |
Statements
A note on Presburger arithmetic with array segments, permutation and equality (English)
0 references
1986
0 references
In this paper, we examine the validity (satisfiability) problem for a language containing Presburger arithmetic, finite length array segments and some fixed second order predicates. In particular, we consider the predicates: PERM, which is used to assert that two array segments contain the same multiset of elements, and \(=\) (equality), which is used to assert that two array segments are identical (i.e., contain the same sequence of elements and have equivalent upper and lower array bounds). It is known that the afore-mentioned (unquantified) language has a decidable validity problem. (In fact, the satisfiability problem is NP- complete.) We consider the case when equality is defined in a seemingly weaker fashion. Let \(Y\simeq B\) be true if and only if array segments A and B contain the same sequence of elements. This definition of equality is more useful in the verification conditions of programs that manipulate queues and/or strings. However, we show that when this form of equality replaces the earlier variety in the previously mentioned language, the validity problem becomes undecidable.
0 references
second order predicates
0 references
validity problem
0 references
satisfiability problem
0 references