Zobrazeno 1 - 10
of 97
pro vyhledávání: '"Moore, J. Strother"'
Autor:
Kaufmann, Matt, Moore, J Strother
Publikováno v:
EPTCS 393, 2023, pp. 67-81
The experience of an ACL2 user generally includes many failed proof attempts. A key to successful use of the ACL2 prover is the effective use of tools to debug those failures. We focus on changes made after ACL2 Version 8.5: the improved break-rewrit
Externí odkaz:
http://arxiv.org/abs/2311.08856
Publikováno v:
EPTCS 359, 2022, pp. 61-75
VWSIM is a circuit simulator for rapid, single-flux, quantum (RSFQ) circuits. The simulator is designed to model and simulate primitive-circuit devices such as capacitors, inductors, Josephson Junctions, and can be extended to simulate other circuit
Externí odkaz:
http://arxiv.org/abs/2205.11698
Autor:
Kaufmann, Matt, Moore, J Strother
Publikováno v:
EPTCS 327, 2020, pp. 16-31
Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- provides direct support for iteration. We describe an ACL2 analogue loop$
Externí odkaz:
http://arxiv.org/abs/2009.13762
Autor:
Moore, J. Strother
Publikováno v:
EPTCS 192, 2015, pp. 93-109
When ACL2 is used to model the operational semantics of computing machines, machine states are typically represented by terms recording the contents of the state components. When models are realistic and are stepped through thousands of machine cycle
Externí odkaz:
http://arxiv.org/abs/1509.06084
Autor:
Kaufmann, Matt, Moore, J Strother
Publikováno v:
EPTCS 152, 2014, pp. 1-7
We report on improvements to ACL2 made since the 2013 ACL2 Workshop.
Comment: In Proceedings ACL2 2014, arXiv:1406.1238
Comment: In Proceedings ACL2 2014, arXiv:1406.1238
Externí odkaz:
http://arxiv.org/abs/1406.1556
Autor:
Moore, J Strother, Wirth, Claus-Peter
Publikováno v:
IfCoLog Journal of Logics and their Applications, Vol. 4, number 5, pp. 1505-1634 (2017)
We review the history of the automation of mathematical induction
Comment: ii+107 pages
Comment: ii+107 pages
Externí odkaz:
http://arxiv.org/abs/1309.6226
Autor:
Kaufmann, Matt, Moore, J Strother
Publikováno v:
EPTCS 114, 2013, pp. 5-12
We report on highlights of the ACL2 enhancements introduced in ACL2 releases since the 2011 ACL2 Workshop. Although many enhancements are critical for soundness or robustness, we focus in this paper on those improvements that could benefit users who
Externí odkaz:
http://arxiv.org/abs/1304.7855
Autor:
Kaufmann, Matt, Moore, J Strother
Publikováno v:
EPTCS 70, 2011, pp. 46-60
The last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-event', 'mbe', and trust tags. In this paper we provide user-level summ
Externí odkaz:
http://arxiv.org/abs/1110.4673