Deciding Predicate Logical Theories of Real-Valued Functions

TL;DR

This paper introduces a first-order predicate language for reasoning about multi-dimensional smooth real-valued functions and their derivatives, showing that some positive decidability results are achievable despite known undecidability barriers.

Contribution

It defines a new logical framework for real-valued functions and proves that certain decision problems are decidable within this framework, overcoming previous barriers.

Findings

Defined a predicate language for smooth real functions

Established positive decidability results for certain theories

Demonstrated decidability despite undecidability barriers

Abstract

The notion of a real-valued function is central to mathematics, computer science, and many other scientific fields. Despite this importance, there are hardly any positive results on decision procedures for predicate logical theories that reason about real-valued functions. This paper defines a first-order predicate language for reasoning about multi-dimensional smooth real-valued functions and their derivatives, and demonstrates that - despite the obvious undecidability barriers - certain positive decidability results for such a language are indeed possible.