Title: Efficient Support for Common Relations in Lightweight Formal Reasoning Systems

Author: Andrei Lapets and David House

Date: November 6, 2009

Abstract:

In work that involves mathematical rigor, there are numerous benefits to
adopting a representation of models and arguments that can be supplied to a
formal reasoning or verification system: reusability, automatic evaluation
of examples, and verification of consistency and correctness. However,
accessibility has not been a priority in the design of formal verification
tools that can provide these benefits. In earlier work [BUCS-TR-2009-015],
we attempt to address this broad problem by proposing several specific
design criteria organized around the notion of a natural context: the sphere
of awareness a working human user maintains of the relevant constructs,
arguments, experiences, and background materials necessary to accomplish the
task at hand. This work expands one aspect of our earlier work by further
developing an essential capability for any formal reasoning system whose
design is oriented around simulating the natural context: native support for
a collection of mathematical relations that deal with common constructs in
arithmetic and set theory. We provide a formal definition for a context of
relations that can be used to both validate and assist formal reasoning
activities. We provide a proof that any data structure that faithfully
implements this formal notion has an update algorithm that necessarily
converges. Finally, we present and prove the efficiency of an implementation
of such a data structure that leverages modular implementations of two
existing general-purpose data structures: balanced search trees and
transitive closures of hypergraphs.