Instantiation Schemes for Nested Theories

TL;DR

This paper explores how to combine instantiation-based proof procedures in nested configurations to develop new methods for richer theories, with a focus on applications in verification and array theory extensions.

Contribution

It introduces conditions for nesting instantiation procedures, enabling the construction of advanced proof methods for complex theories.

Findings

Established conditions for nested instantiation procedures

Demonstrated application to array theory extensions

Enhanced proof construction techniques for verification

Abstract

This paper investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays.