TY - GEN
T1 - Formalization of asymptotic notations in HOL4
AU - Iqbal, Nadeem
AU - Hasan, Osman
AU - Siddique, Umair
AU - Awwad, Falah
N1 - Funding Information:
ACKNOWLEDGEMENT This work is supported by ICT Fund UAE, fund number 21N206 at UAE University, Al Ain, United Arab Emirates.
Funding Information:
This work is supported by ICT Fund UAE, fund number 21N206 at UAE University, Al Ain, United Arab Emirates.
Publisher Copyright:
© 2019 IEEE.
PY - 2019/2
Y1 - 2019/2
N2 - Asymptotic notations characterize the limiting behavior of a function. They are extensively used in many branches of mathematics and computer science particularly in analytical number theory, combinatorics and computational complexity while analyzing algorithms. Traditionally, the mathematical analysis involving these notations has been done by paper-and-pencil proof methods or simulation. In order to introduce formal verification in this domain, this paper provides the higher-order-logic formalizations of O, Θ, Ω, o and ω notations and the formal verification of most of their classical properties of interest. The formalization is based on the theory of sets, real and natural numbers and has been done using the HOL4 theorem prover.
AB - Asymptotic notations characterize the limiting behavior of a function. They are extensively used in many branches of mathematics and computer science particularly in analytical number theory, combinatorics and computational complexity while analyzing algorithms. Traditionally, the mathematical analysis involving these notations has been done by paper-and-pencil proof methods or simulation. In order to introduce formal verification in this domain, this paper provides the higher-order-logic formalizations of O, Θ, Ω, o and ω notations and the formal verification of most of their classical properties of interest. The formalization is based on the theory of sets, real and natural numbers and has been done using the HOL4 theorem prover.
KW - Asymptotic notations
KW - Formal methods
KW - Higher-order logic
KW - Theorem proving
UR - http://www.scopus.com/inward/record.url?scp=85072949396&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85072949396&partnerID=8YFLogxK
U2 - 10.1109/CCOMS.2019.8821642
DO - 10.1109/CCOMS.2019.8821642
M3 - Conference contribution
AN - SCOPUS:85072949396
T3 - 2019 IEEE 4th International Conference on Computer and Communication Systems, ICCCS 2019
SP - 383
EP - 387
BT - 2019 IEEE 4th International Conference on Computer and Communication Systems, ICCCS 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 4th IEEE International Conference on Computer and Communication Systems, ICCCS 2019
Y2 - 23 February 2019 through 25 February 2019
ER -