|
|
|---|
|
|
|
|---|
SOFT (Second-Order Functions and Theorems) is a tool to mimic second-order functions and theorems in the first-order logic of ACL2.
In SOFT,
second-order functions are mimicked
by first-order functions that depend on
explicitly designated uninterpreted functions
that mimic function variables.
First-order theorems over these second-order functions
mimic second-order theorems universally quantified over function variables.
Instances of second-order functions and theorems
are systematically generated
by replacing function variables with functions.
Theorem instances are proved automatically,
via automatically generated
SOFT does not extend the ACL2 logic. It is a library that provides macros to introduce function variables, second-order functions, second-order theorems, and instances thereof. The macros modify the ACL2 state only by submitting sound and conservative events; they cannot introduce unsoundness or inconsistency on their own.
The
ACL2-2015 Workshop paper on SOFT
provides
an overview of the SOFT macros and some simple examples of their use,
a description of the use of SOFT in program refinement,
and a discussion of related and future work.
The presentation of the Workshop talk is available
here.
The examples from the paper are in community book