D. Basin (2005):
Rippling: Meta-level Guidance for Mathematical Reasoning.
Cambridge University Press.
C. Bishop (2006):
Pattern Recognition and Machine Learning.
Springer.
B. Brock, M. Kaufmann & J S. Moore (1996):
ACL2 Theorems about Commercial Microprocessors.
In: 1st International Conference on Formal Methods in Computer-Aided Design (FMCAD'96),
LNCS 1166,
pp. 275–293,
doi:10.1007/BFb0031816.
H. Chamarthi, P. Dillinger, M. Kaufmann & P. Manolios (2011):
Integrating Testing and Interactive Theorem Proving.
In: 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'11),
EPTCS 70,
pp. 4–19,
doi:10.4204/EPTCS.70.1.
K. Claessen (2013):
Automating Inductive Proofs using Theory Exploration.
In: 24th International Conference on Automated Deduction (CADE-24),
LNCS 7898,
pp. 392–406,
doi:10.1007/978-3-642-38574-2_27.
S. Colton (2002):
The HR Program for Theorem Generation.
In: 18th International Conference on Automated Deduction (CADE-18),
LNCS 2392,
pp. 285–289,
doi:10.1007/3-540-45620-1_24.
J. Davis:
ACL2 Community Books.
https://code.google.com/p/acl2-books/.
J. Davis (2009–2014):
XDOC Documentation System for ACL2.
http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/.
J. Denzinger, M. Fuchs, C. Goller & S. Schulz (1999):
Learning from Previous Proof Experience: A Survey.
Technical Report.
Technische Universitat Munchen.
J. Denzinger & S. Schulz (2000):
Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts.
Information and Computation 162(1-2),
pp. 59–79,
doi:10.1006/inco.1999.2857.
C. Eastlund, D. Vaillancourt & M. Felleisen (2007):
ACL2 for Freshmen: First Experiences.
In: 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'07),
ACM Press,
pp. 200–211.
D. Greve (2008):
Efficient Execution in an Automated Reasoning Environment.
Journal of Functional Programming 18(1),
pp. 15–46,
doi:10.1017/S0956796807006338.
M. Hall (2009):
The WEKA Data Mining Software: An Update.
SIGKDD Explorations 11(1),
pp. 10–18,
doi:10.1145/1656274.1656278.
J. Heras & E. Komendantskaya (2013–2014):
ACL2(ml): downloadable programs, manual, examples.
http://staff.computing.dundee.ac.uk/katya/ACL2ml.
J. Heras, E. Komendantskaya, M. Johansson & E. Maclean (2013):
Proof-Pattern Recognition and Lemma Discovery in ACL2.
In: 19th Logic for Programming Artificial Intelligence and Reasoning (LPAR-19),
LNCS 8312,
pp. 389–406,
doi:10.1007/978-3-642-45221-5_27.
S. Hetzl, A. Leitsch & D. Weller (2012):
Towards Algorithm Cut-Introduction.
In: 18th Logic for Programming Artificial Intelligence and Reasoning (LPAR-18),
LNCS 7180,
pp. 228–242,
doi:10.1007/978-3-642-28717-6_19.
M. Johansson, L. Dixon & A. Bundy (2011):
Conjecture Synthesis for Inductive Theories.
Journal of Automated Reasoning 47(3),
pp. 251–289,
doi:10.1007/s10817-010-9193-y.
M. Kaufmann, P. Manolios & J S. Moore (2000):
Computer-Aided Reasoning: ACL2 Case Studies.
Kluwer Academic Publishers,
doi:10.1007/978-1-4757-3188-0.
M. Kaufmann, P. Manolios & J S. Moore (2000):
Computer-Aided Reasoning: An approach.
Kluwer Academic Publishers,
doi:10.1007/978-1-4615-4449-4.
D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban & T. Heskes (2012):
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics.
In: 6th International Joint Conference on Automated Reasoning (IJCAR'12),
LNCS 7364,
pp. 378–392,
doi:10.1007/978-3-642-31365-3_30.
R. L. McCasland, A. Bundy & P. F. Smith (2006):
Ascertaining Mathematical Theorems.
In: 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005),
ENTCS 151,
pp. 21–38,
doi:10.1016/j.entcs.2005.11.021.
O. Montano-Rivas, R. Mccasland, L. Dixon & A. Bundy (2012):
Scheme-based theorem discovery and concept invention.
Expert Systems with Applications 39(2),
pp. 1637–1646,
doi:10.1016/j.eswa.2011.06.055.
R. Page (2007):
Engineering Software Correctness.
Journal of Functional Programming 17(6),
pp. 675–686,
doi:10.1017/S095679680700634X.
E. Tsivtsivadze, J. Urban, H. Geuvers & T. Heskes (2011):
Semantic Graph Kernels for Automated Reasoning.
In: SIAM Conference on Data Mining (SDM'11).
SIAM / Omnipress,
pp. 795–803,
doi:10.1137/1.9781611972818.68.
J. Urban, G. Sutcliffe, P. Pudlák & J. Vyskocil (2008):
MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance.
In: 4th International Joint Conference on Automated Reasoning (IJCAR'08),
LNCS 5195,
pp. 441–456,
doi:10.1007/978-3-540-71070-7_37.
N. Wetzler & M. Kaufmann (2014):
Remove-hyps and Writing Utilities with Make-event.
ACL2 Theorem Proving Seminar. University of Texas.
eptcs@eptcs.org