APPLYING AN INTERACTIVE PROGRAM-PROVER LIKE COQ CAN BECOME A NEW STANDARD FOR APPROBING OF PRACTICALLY IMPORTANT THEORETICAL WORKS

N. D. Stukach

Abstract


There are some theories in the world, which have great scientific and practical importance but have no approbation. In the article the theory of “widened long flip-flop” (that represents scientific and practical interests in the field of building mission-critical computing system) is used as an example to analyze reasons of such situation and ways of solving this issue. These ways appear with powerful interactive program-prover like Coq. Such prover may either prove or do not prove the theory since it depends on human prompts. But if the proof is successful, the correctness of the theory will be guaranteed.

Key words: complex theory, approbation, program-prover, Coq, arXiv.org

Стукач Н. Д. Применение интерактивной программы-прувера типа Coq может стать новым стандартом апробации практически важных теоретических работ/ Национальный авиационный университет, Украина, Киев

В мире существуют теории, имеющие важное научное и практическое значение, но не имеющие апробации. В статье на примере теории «длинного триггера» (2008 г.), представляющей научный и практический интерес в области создания mission-critical вычислительных систем, анализируются причины такой ситуации, а также возможности выхода из неё, возникающие в связи с появлением мощных интерактивных программ-пруверов типа Coq. Прувер может доказать или не доказать теорию, многое зависит от подсказок человека. Но в случае, если доказательство удалось, корректность теории будет гарантирована.

Ключевые слова: сложная теория, апробация, программа-прувер, Coq, arXiv.org


Full Text:

PDF

References


Stukach, Nick (2008). Easily testable logical networks based on a «widened long flip-flop».

. (2019, апрель, 08).

Coq (Материал из Википедии — свободной энциклопедии). . (2019, апрель, 08).

The Software Foundations. Volumes 1 to 4. . (2019, апрель, 08).

О машинном доказательстве теорем. . (2019, апрель, 08).

Gonthier, Georges (2008), «Formal Proof—The Four-Color Theorem» (PDF), Notices of the American Mathematical Society, 55 (11), pp. 1382–1393, MR 2463991.

References:

Stukach, Nick (2008). Easily testable logical networks based on a «widened long flip-flop». Retrieved from https://arxiv.org/ftp/arxiv/papers/0808/0808.2602.pdf. (2019, April, 08).

Coq (From Wikipedia, the free encyclopedia). Retrieved from https://en.wikipedia.org/wiki/Coq. (2019, April, 08).

The Software Foundations. Volumes 1 to 4. Retrieved from https://softwarefoundations.cis.upenn.edu/current/index.html (2019, April, 08).

О mashinnom dokazatelstve teorem [On machine proving of theorems]. Retrieved from

https://itc.ua/articles/o_mashinnom_dokazatelstve_teorem_26341/ [in Russian]. (2019, April, 08).

Gonthier, Georges (2008), «Formal Proof—The Four-Color Theorem» (PDF), Notices of the American Mathematical Society, 55 (11), pp. 1382–1393, MR 2463991.




DOI: https://doi.org/10.26886/2520-7474.2(34)2019.6

Refbacks

  • There are currently no refbacks.