На основі аксіоматичної системи специфікацій програм над метаномінативними даними побудовано прототип системи автоматизації доведення теорем теорія МНД. Продемонстровано, що система дозволяє доводити властивості програм.
Ключові слова: Обчислюваність, обчислювані функції, ординал, семантика програм, частково обчислювані функції.
The prototype of automatic theorem prover is constructed for the axiomatic system of program specification over metanominative data. Is shown thai the system permits to proveproperties of the programs.
Key Words: Computability, computable Junctions, ordinal, semantics of the programs, partially computable functions.
