Combinatory Array Logic with Sums

TL;DR

This paper establishes an NP upper bound for a logic involving integer arrays with sums and ordering, extending combinatory array logic, and compares its expressiveness and complexity with other fragments.

Contribution

It introduces a new NP-bounded fragment of array logic that includes sums and ordering, and provides a comparative analysis with existing fragments.

Findings

Proves NP upper bound for the extended array logic.

Shows the expressiveness of the new fragment.

Provides a complexity comparison with seven other fragments.

Abstract

We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combinatory array logic with an ordering relation on the index set and the ability to express sums of elements. We compare our fragment with seven other fragments in the literature in terms of their expressiveness and computational complexity.