References

  1. 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.
  2. R. S. Boyer & J S. Moore (1997): A Computational Logic Handbook, Second Edition. Academic Press, New York.
  3. M. Kaufmann & \voidb@x J S. Moore (2018): Limited Second-Order Functionality in a First-Order Setting. Journal of Automated Reasoning, doi:10.1007/s10817-018-09505-9. Available at http://www.cs.utexas.edu/users/kaufmann/papers/apply/.
  4. 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.
  5. K. Kunen (1998): Nonconstructive Computational Mathematics. J. Autom. Reason. 21(1), pp. 69–97, doi:10.1023/A:1005888712422.
  6. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org