Quadratic Extensions in ACL2
| Autor: | Ruben Gamboa, Woodrow Gamboa, John Cowles |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Root (chord) Structure (category theory) Field (mathematics) Quadratic function Extension (predicate logic) Logic in Computer Science (cs.LO) Combinatorics Quadratic equation Mathematics::K-Theory and Homology Trigonometric functions Cube root Mathematics |
| DOI: | 10.48550/arxiv.2009.13766 |
| Popis: | 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 = K_0, K_1, K_2, ..., where each K_i+1 is a quadratic extension field of K_i. Moreover, we show that some specific numbers, such as the cube root of 2 and the cosine of pi/9, cannot belong to any of the K_i, simply because of the structure of quadratic extension fields. In particular, this is used to show that the cube root of 2 and cosine of pi/9 are not rational. Comment: In Proceedings ACL2 2020, arXiv:2009.12521 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|