Quadratic Extensions in ACL2

被引：0
|
作者：
Gamboa, Ruben [1 ]
Cowles, John [1 ]
Gamboa, Woodrow [2 ]
机构：
[1] Univ Wyoming, Laramie, WY 82071 USA
[2] Stanford Univ, Stanford, CA USA
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2020年 / 327期
关键词：
D O I：
10.4204/EPTCS.327.6
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Given a field K, a quadratic extension field L is an extension of K that can be generated from K by adding a root of a quadratic polynomial with coefficients in K. This paper shows how ACL2(r) can be used to reason about chains of quadratic extension fields Q = K0 C K1 C K2 C & BULL; & BULL; & BULL;, where each Ki+1 is a quadratic extension field of Ki. Moreover, we show that some specific numbers, such as 3 & RADIC;2 and cos 9 & pi;, cannot belong to any of the Ki, simply because of the structure of quadratic extension fields. In particular, this is used to show that 3 & RADIC;2 and cos 9 & pi; are not rational.
引用
收藏
页码：75 / 86
页数：12
相关论文
共 50 条
  • [1] ACL2
    Gamboa, R
    [J]. SEVENTEEN PROVERS OF THE WORLD, 2006, 3600 : 55 - 66
  • [2] ACL2(ml): Machine-Learning for ACL2
    Heras, Jonathan
    Komendantskaya, Ekaterina
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 61 - 75
  • [3] Iteration in ACL2
    Kaufmann, Matt
    Moore, J. Strother
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (327): : 16 - 31
  • [4] An ACL2 tutorial
    Kaufmann, Matt
    Moore, J. Strother
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2008, 5170 : 17 - +
  • [5] 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
  • [6] 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 - +
  • [7] Hygienic Macros for ACL2
    Eastlund, Carl
    Felleisen, Matthias
    [J]. TRENDS IN FUNCTIONAL PROGRAMMING, 2011, 6546 : 84 - 101
  • [8] 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
  • [9] A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
    Coglio, Alessandro
    [J]. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2022, 359 : 168 - 184
  • [10] Meta reasoning in ACL2
    Hunt, WA
    Kaufmann, M
    Krug, RB
    Moore, JS
    Smith, EW
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2005, 3603 : 163 - 178
12345