R. Boyer & J S. Moore (1988):
The Addition of Bounded Quantification and Partial Functions to a Computational Logic and Its Theorem Prover.
Journal of Automated Reasoning 4(2),
pp. 117–172,
doi:10.1007/BF00244392.
See http://www.cs.utexas.edu/users/moore/publications/quant.pdf.
R. S. Boyer & J S. Moore (1997):
A Computational Logic Handbook, Second Edition.
Academic Press,
New York.
M. Kaufmann, \voidb@x J S. Moore & \voidb@x The ACL2 Community (2020):
The Combined ACL2+Books User's Manual.
http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html.
K. Kunen (1998):
Nonconstructive Computational Mathematics.
J. Autom. Reason. 21(1),
pp. 69–97,
doi:10.1023/A:1005888712422.
J S. Moore (1975):
Introducing Iteration into the Pure LISP Theorem-Prover.
IEEE Transactions on Software Engineering 1(3),
pp. 328–338,
doi:10.1109/TSE.1975.6312857.
See http://www.cs.utexas.edu/users/moore/publications/parc-csl-tr-74-3.pdf.