Implementation of the Composition-nominative Approach to Program Formalization in Mizar
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 whic...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Vladimir Andrunachievici Institute of Mathematics and Computer Science
2018-05-01
|
| Series: | Computer Science Journal of Moldova |
| Subjects: | |
| Online Access: | http://www.math.md/files/csjm/v26-n1/v26-n1-(pp59-76).pdf |
| _version_ | 1811263965241540608 |
|---|---|
| author | Ievgen Ivanov Artur Kornilowicz Mykola Nikitchenko |
| author_facet | Ievgen Ivanov Artur Kornilowicz Mykola Nikitchenko |
| author_sort | Ievgen Ivanov |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-12T19:54:33Z |
| format | Article |
| id | doaj.art-a77c69ab9a394fb7854382c6ba6b81d5 |
| institution | Directory Open Access Journal |
| issn | 1561-4042 |
| language | English |
| last_indexed | 2024-04-12T19:54:33Z |
| publishDate | 2018-05-01 |
| publisher | Vladimir Andrunachievici Institute of Mathematics and Computer Science |
| record_format | Article |
| series | Computer Science Journal of Moldova |
| spelling | doaj.art-a77c69ab9a394fb7854382c6ba6b81d52022-12-22T03:18:42ZengVladimir Andrunachievici Institute of Mathematics and Computer ScienceComputer Science Journal of Moldova1561-40422018-05-01261(76)5976Implementation of the Composition-nominative Approach to Program Formalization in MizarIevgen Ivanov0Artur Kornilowicz1Mykola Nikitchenko2Taras Shevchenko National University of Kyiv, UkraineUniversity of Bialystok, PolandTaras Shevchenko National University of Kyiv, UkraineIn 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.http://www.math.md/files/csjm/v26-n1/v26-n1-(pp59-76).pdfFormal methodsprogram semanticssemistructured dataformalizationproof assistant |
| spellingShingle | Ievgen Ivanov Artur Kornilowicz Mykola Nikitchenko Implementation of the Composition-nominative Approach to Program Formalization in Mizar Computer Science Journal of Moldova Formal methods program semantics semistructured data formalization proof assistant |
| title | Implementation of the Composition-nominative Approach to Program Formalization in Mizar |
| title_full | Implementation of the Composition-nominative Approach to Program Formalization in Mizar |
| title_fullStr | Implementation of the Composition-nominative Approach to Program Formalization in Mizar |
| title_full_unstemmed | Implementation of the Composition-nominative Approach to Program Formalization in Mizar |
| title_short | Implementation of the Composition-nominative Approach to Program Formalization in Mizar |
| title_sort | implementation of the composition nominative approach to program formalization in mizar |
| topic | Formal methods program semantics semistructured data formalization proof assistant |
| url | http://www.math.md/files/csjm/v26-n1/v26-n1-(pp59-76).pdf |
| work_keys_str_mv | AT ievgenivanov implementationofthecompositionnominativeapproachtoprogramformalizationinmizar AT arturkornilowicz implementationofthecompositionnominativeapproachtoprogramformalizationinmizar AT mykolanikitchenko implementationofthecompositionnominativeapproachtoprogramformalizationinmizar |