References

  1. ACL2 Community (Accessed: 2018): ACL2+Books Documentation. Available at http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html.
  2. Tomáš Balyo, Armin Biere, Markus Iser & Carsten Sinz (2016): SAT Race 2015. Artificial Intelligence 241, pp. 45–65, doi:10.1016/j.artint.2016.08.007.
  3. Tomáš Balyo, Marijn J. H. Heule & Matti Järvisalo (2017): Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. Publication series B B-2017-1. University of Helsinki, Department of Computer Science. Available at http://hdl.handle.net/10138/224324.
  4. Robert S. Boyer, David M. Goldschlag, Matt Kaufmann & J Strother Moore (1991): Functional instantiation in first-order logic. In: Vladimir Lifschitz: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy. Academic Press, Inc., pp. 7–26, doi:10.1016/B978-0-12-450010-5.50007-4.
  5. Jared Davis & Sol Swords (2013): Verified AIG Algorithms in ACL2. In: Ruben Gamboa & Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, Laramie, Wyoming, USA , May 30-31, 2013, Electronic Proceedings in Theoretical Computer Science 114. Open Publishing Association, pp. 95–110, doi:10.4204/EPTCS.114.8.
  6. Shilpi Goel, Warren A Hunt, Jr. & Matt Kaufmann (2013): Abstract Stobjs and Their Application to ISA Modeling. In: Ruben Gamboa & Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, Laramie, Wyoming, USA , May 30-31, 2013, Electronic Proceedings in Theoretical Computer Science 114. Open Publishing Association, pp. 54–69, doi:10.4204/EPTCS.114.5.
  7. Matt Kaufmann, J Strother Moore, Sandip Ray & Erik Reeber (2009): Integrating external deduction tools with ACL2. Journal of Applied Logic 7(1), pp. 3 – 25, doi:10.1016/j.jal.2007.07.002. Special Issue: Empirically Successful Computerized Reasoning.
  8. Alan Mishchenko, Satrajit Chatterjee, Robert Brayton & Niklas Een (2006): Improvements to Combinational Equivalence Checking. In: Proceedings of the 2006 IEEE/ACM International Conference on Computer-aided Design, ICCAD '06. ACM, New York, NY, USA, pp. 836–843, doi:10.1145/1233501.1233679.
  9. Yan Peng & Mark R. Greenstreet (2015): Extending ACL2 with SMT Solvers. In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 61–77, doi:10.4204/EPTCS.192.6.
  10. Erik Reeber & Warren A. Hunt (2006): A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 453–467, doi:10.1007/11814771_38.
  11. J. Sawada & E. Reeber (2006): ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool. In: 2006 Formal Methods in Computer Aided Design, pp. 161–170, doi:10.1109/FMCAD.2006.3.
  12. Sol Swords & Jared Davis (2011): Bit-Blasting ACL2 Theorems. In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 84–102, doi:10.4204/EPTCS.70.7.
  13. G. S. Tseitin (1983): Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, chapter On the Complexity of Derivation in Propositional Calculus, pp. 466–483. Springer, Berlin, Heidelberg, doi:10.1007/978-3-642-81955-1_28.

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