Inspirel banner

Supporting Quantified Statements - Part 1

This article belongs to the series documenting the reasoning behind and development of new features in the Formal Methods Toolkit.

Quantified statements are very powerful tools in the area of formal methods, as they allow to express (and verify) knowledge that binds together multiple elements. Quantified statements involve existential and universal quantifiers and allow to state things such as:

In other words, quantified statements are essential for expressing requirements and for proving correctness of programs that deal with arrays, which are the most straightforward collections of objects treated together. Still, they were not supported in the first FMT release - this article sketches the ideas on what kind of support is needed.

Even though Mathematica recognizes both Exists and ForAll symbols (with very nice formatting), they are not automatically understood in all contexts and some work is necessary to integrate them with the existing FMT framework. The most fundamental building blocks are:

Further articles in this mini-series will demonstrate the integration of these features in the FMT framework.