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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.