A decision method for the integrability of differential-algebraic Pfaffian systems

TL;DR

This paper introduces an effective decision method for determining the integrability of differential-algebraic Pfaffian systems, with a proven complexity bound and implications for the differential Nullstellensatz.

Contribution

It provides a novel integrability criterion and a decision procedure with a triple exponential complexity bound for differential-algebraic Pfaffian systems.

Findings

Effective integrability criterion established

Decision method with triple exponential complexity bound

Upper bound for differentiation order in differential Nullstellensatz

Abstract

We prove an effective integrability criterion for differential-algebraic Pfaffian systems leading to a decision method of consistency with a triple exponential complexity bound. As a byproduct, we obtain an upper bound for the order of differentiations in the differential Nullstellensatz for these systems.