Computer Science Journal of Moldova (May 2018)

Implementation of the Composition-nominative Approach to Program Formalization in Mizar

  • Ievgen Ivanov,
  • Artur Kornilowicz,
  • Mykola Nikitchenko

Journal volume & issue
Vol. 26, no. 1(76)
pp. 59 – 76

Abstract

Read online

In this paper we describe an ongoing work on implementation of the composition-nominative approach to program formalization in Mizar proof assistant based on the first-order logic and axiomatic set theory. The further aim of this work is development of a formal verification tool for software which processes and communicates with complex forms of data.

Keywords