Limited Second-Order Functionality in a First-Order Setting

Here is a copy of our paper, "Limited Second-Order Functionality in a First-Order Setting", which is the Author's Accepted Manuscript (AAM), defined by the publisher, Springer, as follows.

This is a post-peer-review, pre-copyedit version of an article published in Journal of Automated Reasoning. The final authenticated version is available online at:

Here is a view-only copy of the published paper. Springer says: "If ... an individual can view content via a personal or institutional subscription, recipients of the link will also be able to download and print the PDF. All readers of your article via the shared link will also be able to use Enhanced PDF features such as annotation tools, one-click supplements, citation file exports and article metrics."

The latest version of the corresponding books (under the ACL2 community books on GitHub) may be found by following this link.

Matt Kaufmann
J Strother Moore