Zobrazeno 1 - 10
of 65
pro vyhledávání: '"John Cowles"'
Autor:
Ruben Gamboa, John Cowles
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 280, Iss Proc. ACL2 2018, Pp 98-110 (2018)
We report on a verification of the Fundamental Theorem of Algebra in ACL2(r). The proof consists of four parts. First, continuity for both complex-valued and real-valued functions of complex numbers is defined, and it is shown that continuous functio
Externí odkaz:
https://doaj.org/article/16a22f65ae4d48fe8102e9871d5faf5d
Autor:
John Cowles, Ruben Gamboa
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 249, Iss Proc. ACL2Workshop 2017, Pp 18-29 (2017)
The Cayley-Dickson Construction is a generalization of the familiar construction of the complex numbers from pairs of real numbers. The complex numbers can be viewed as two-dimensional vectors equipped with a multiplication. The construction can be
Externí odkaz:
https://doaj.org/article/d185fbc8b361408388817e6abf83d902
Autor:
John Cowles, Ruben Gamboa
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 192, Iss Proc. ACL2 2015, Pp 53-59 (2015)
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 < 1 + 2 + 3 + 4
Externí odkaz:
https://doaj.org/article/2c298a52a8f44dbdb0e0f18829fc94ff
Autor:
Ruben Gamboa, John Cowles
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 152, Iss Proc. ACL2 2014, Pp 101-110 (2014)
The verification of many algorithms for calculating transcendental functions is based on polynomial approximations to these functions, often Taylor series approximations. However, computing and verifying approximations to the arctangent function are
Externí odkaz:
https://doaj.org/article/eaf1afb115184fdfa3ebd2c1fde6151a
Autor:
John Cowles, Ruben Gamboa
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 152, Iss Proc. ACL2 2014, Pp 89-100 (2014)
ACL2(r) is a variant of ACL2 that supports the irrational real and complex numbers. Its logical foundation is based on internal set theory (IST), an axiomatic formalization of non-standard analysis (NSA). Familiar ideas from analysis, such as continu
Externí odkaz:
https://doaj.org/article/4398a03fc27a4dc2bdd1cf73b0161aa9
Autor:
Mihkel Kaljurand, Laimutis Telksnys, Gintarė Naujokaitytė, Jelena Gorbatsova, Vidmantas Stanys, John Cowles, Audrius Maruška, Tomas Drevinskas
Publikováno v:
Chemija. 31
Capillary electrophoresis often causes unrepeatable peak migration times in the electropherogram due to changes of electroosmosis, yet in some cases this separation technique does not have a replacement alternative. Some attempts to overcome this iss
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::442024f9b39b4d42f75da0adfa8f4714
https://doi.org/10.6001/chemija.v31i3.4288
https://doi.org/10.6001/chemija.v31i3.4288
Autor:
John Cowles, Ruben Gamboa
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 280, Iss Proc. ACL2 2018, Pp 98-110 (2018)
We report on a verification of the Fundamental Theorem of Algebra in ACL2(r). The proof consists of four parts. First, continuity for both complex-valued and real-valued functions of complex numbers is defined, and it is shown that continuous functio
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::969c5ca795bc24d1724b183751519c33
https://doi.org/10.4204/eptcs.280.8
https://doi.org/10.4204/eptcs.280.8
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
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::eb910104bc080e67f467275b0ca99257
Publikováno v:
NORCAS
Mitchell's method typically is used to compute approximate base-2 antilogarithms using minimal hardware (no ROM). Another use of identical hardware approximates the function (called the “addition logarithm”) that computes the sum of values repres
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7cb81615d7173cf8a2213b114b81365d
https://doi.org/10.1109/norchip.2019.8906904
https://doi.org/10.1109/norchip.2019.8906904
Publikováno v:
ARITH
The Residue Number System (RNS) offers fast and cheap carry-free integer arithmetic but has slow and expensive overflow detection. The Logarithmic Number System (LNS) offers fast real multiplication, division and powers with floating-point-like relat
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e22d24f585a4ce30814574b4f486e788
https://doi.org/10.1109/arith.2019.00030
https://doi.org/10.1109/arith.2019.00030