Reasoning on Schemata of Formulae

TL;DR

This paper introduces a logic for reasoning about complex sequences of formulae, called schemata, over various algebraic structures, with a proof procedure that ensures soundness, completeness, and termination.

Contribution

It presents a novel logic and proof procedure for reasoning on inductively defined schemata, extending the computational properties of base languages.

Findings

Proof procedure is sound, complete, and terminating

Satisfiability of schemata reduces to finite disjunctions of base formulae

Computational properties of base language extend to schemata

Abstract

A logic is presented for reasoning on iterated sequences of formulae over some given base language. The considered sequences, or "schemata", are defined inductively, on some algebraic structure (for instance the natural numbers, the lists, the trees etc.). A proof procedure is proposed to relate the satisfiability problem for schemata to that of finite disjunctions of base formulae. It is shown that this procedure is sound, complete and terminating, hence the basic computational properties of the base language can be carried over to schemata.