Perfect Numbers in ACL2

被引：0
|
作者：
Cowles, John [1 ]
Gamboa, Ruben [1 ]
机构：
[1] Univ Wyoming, Dept Comp Sci, Laramie, WY 82071 USA
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2015年 / 192期
关键词：
D O I：
10.4204/EPTCS.192.5
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A perfect number is a positive integer n such that n equals the sum of all positive integer divisors of n that are less than n. That is, although n is a divisor of n, n is excluded from this sum. Thus 6 = 1 + 2 + 3 is perfect, but 12 not equal 1 + 2 + 3 + 4 + 6 is not perfect. An ACL2 theory of perfect numbers is developed and used to prove, in ACL2(r), this bit of mathematical folklore: Even if there are infinitely many perfect numbers, the series below, of the reciprocals of all perfect numbers, converges. Sigma(perfectn) 1/n
引用
收藏
页码：53 / 59
页数：7
相关论文
共 50 条
  • [1] Verifying Sierpinski and Riesel Numbers in ACL2
    Cowles, John R.
    Gamboa, Ruben
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (70): : 20 - 27
  • [2] ACL2
    Gamboa, R
    [J]. SEVENTEEN PROVERS OF THE WORLD, 2006, 3600 : 55 - 66
  • [3] ACL2(ml): Machine-Learning for ACL2
    Heras, Jonathan
    Komendantskaya, Ekaterina
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 61 - 75
  • [4] ACL2
    [J]. Lect. Notes Comput. Sci., 2006, (55-66):
  • [5] Iteration in ACL2
    Kaufmann, Matt
    Moore, J. Strother
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (327): : 16 - 31
  • [6] How Can I Do That with ACL2? Recent Enhancements to ACL2
    Kaufmann, Matt
    Moore, J. Strother
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (70): : 46 - 60
  • [7] An ACL2 tutorial
    Kaufmann, Matt
    Moore, J. Strother
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2008, 5170 : 17 - +
  • [8] ACL2s: "The ACL2 sedan"
    Dillinger, Peter C.
    Manolios, Panagiotis
    Vroon, Daron
    Moore, J. Strother
    [J]. 29TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: ICSE 2007 COMPANION VOLUME, PROCEEDINGS, 2007, : 59 - +
  • [9] Hygienic Macros for ACL2
    Eastlund, Carl
    Felleisen, Matthias
    [J]. TRENDS IN FUNCTIONAL PROGRAMMING, 2011, 6546 : 84 - 101
  • [10] ACL2s: "The ACL2 Sedan"
    Dillinger, Peter C.
    Manolios, Panagiotis
    Vroon, Daron
    Moore, J. Strother
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 174 (02) : 3 - 18
12345