Formalization of asymptotic notations in HOL4

Nadeem Iqbal, Osman Hasan, Umair Siddique, Falah Awwad

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publication2019 IEEE 4th International Conference on Computer and Communication Systems, ICCCS 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages383-387
Number of pages5
ISBN (Electronic)9781728113227
DOIs
Publication statusPublished - Feb 2019
Event4th IEEE International Conference on Computer and Communication Systems, ICCCS 2019 - Singapore, Singapore
Duration: Feb 23 2019Feb 25 2019

Publication series

Name2019 IEEE 4th International Conference on Computer and Communication Systems, ICCCS 2019

Conference

Conference4th IEEE International Conference on Computer and Communication Systems, ICCCS 2019
Country/TerritorySingapore
CitySingapore
Period2/23/192/25/19

Keywords

  • Asymptotic notations
  • Formal methods
  • Higher-order logic
  • Theorem proving

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computer Networks and Communications
  • Computer Vision and Pattern Recognition
  • Information Systems

Fingerprint

Dive into the research topics of 'Formalization of asymptotic notations in HOL4'. Together they form a unique fingerprint.

Cite this