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 条

[31] Rewriting with Equivalence Relations in ACL2
Bishop Brock
Matt Kaufmann
J Strother Moore
[J]. Journal of Automated Reasoning, 2008, 40 : 293 - 306
[32] Implementing an Automatic Differentiator in ACL2
Reid, Peter
Gamboa, Ruben
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (70): : 61 - 69
[33] A Simple Java']Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java']Java
Coglio, Alessandro
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (280): : 1 - 17
[34] Linear and nonlinear arithmetic in ACL2
Hunt, WA
Krug, RB
Moore, J
[J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 319 - 333
[35] Modeling Algorithms in SystemC and ACL2
O'Leary, John W.
Russinoff, David M.
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 145 - 162
[36] A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
Coglio, Alessandro
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (359): : 185 - 201
[37] Symbolic simulation and verification of VHDL with ACL2
Borrione, D
Georgelin, P
[J]. SYSTEM-ON-CHIP METHODOLOGIES & DESIGN LANGUAGES, 2001, : 59 - 69
[38] The Cayley-Dickson Construction in ACL2
Cowles, John
Gamboa, Ruben
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (249): : 18 - 29
[39] Integrating external deduction tools with ACL2
Kaufmann, Matt
Moore, J. Strother
Ray, Sandip
Reeber, Erik
[J]. JOURNAL OF APPLIED LOGIC, 2009, 7 (01) : 3 - 25
[40] Proceedings - 17th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2022
[J]. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2022, 359

← 1 2 3 4 5 →