Логіко-дедуктивне обгрунтування програмування

Реферат на тему:

Логіко-дедуктивне обґрунтування програмування

У міру нагромадження й ускладнення наукових знань виникла необхідність їхнього упорядкування, структурної побудови, установлення зв’язків між елементами, розкриття їхніх основних принципів, понять, надання цим знанням строгої науковості й визначеності.

У вирішенні цих питань необхідні системний аналіз і структурна побудова наукового знання. Вперше в історії науки системно-структурний аналіз у діяльності людського мислення і його кодування провів Аристотель. Він сформулював закони правильного мислення — закони логіки — і вперше у вигляді системи наукового знання побудував формальну логіку. До Аристотеля існували окремі логічні фрагменти і положення, але не було точної, стрункої системи логічної побудови. Сам Аристотель говорить про це: «Що стосується вчення про умовиводи, то ми не знайшли нічого такого, що було б сказано до нас, а мали самі створювати його з більшою затратою часі та сил» [1, 593].

Формальна логіка стала теоретичною основою в побудові дедуктивних теорій і її вищої форми — форми побудови аксіоматичних систем. Аксіоматичні системи пройшли три етапи розвитку: конкретно змістовний, абстрактно змістовний або напівформальний і формальний. Зразком першої аксіоматичної системи є «Начала» Евкліда, механіка Ньютона, аналітична механіка Лагранжаабстрактно змістовну аксіоматику являє собою аксіоматика арифметики Пеанозразком третьої аксіоматичної системи є аксіоматика математичної логіки, формальної арифметики, теорії ймовірностей А. Н. Колмогорова. Усі ці види аксіоматичних систем покликані до життя потребами наукового знання, що розвивається, а також для розв’язання внутрішніх протиріч, що виникають у процесі розвитку дедуктивних наук.

Конкретно змістовна аксіоматика будується на інтуїтивній основі. Несуворий підхід існує і до принципів побудови дедуктивних наук (несуперечності, повноти, незалежності), а також і до ідеї доказу. Але ця перша аксіоматична система сприяла систематизації наукового знання, являла собою цілісне, закінчене наукове знання. Аксіоматика Евкліда очистила геометричну теорію від повторів, протиріч і представила всю теоретичну систему в найбільш простій і доказовій формі. Але ця аксіоматика має ряд недоліків: вона «схоплює» найпростіші відносини між предметами і явищами об'єктивної дійсності, віднесена лише до одних геометричних об'єктів, до однієї предметної галузі, має слабку синтетичність. Основою цієї аксіоматичної системи є формальна логіка Аристотеля.

З розвитком математики і теоретичного природознавства статична аксіоматична система Евкліда перестала задовольняти подальші вимоги. З уведенням змінної величини й відкриттям неевклідових геометрій необхідною стала така логічна операція, яка виконувала б побудову математичної теорії на абстрактно змістовній основі й мала б інтерпретацію. Інтерпретації можуть бути різного роду і мати різний зміст, але елементи аксіоматичної системи далекі від конкретної змістовної основи і мають широкий абстрактний зміст. Так, при побудові абстрактно змістовної аксіоматичної системи Д. Гільберт указує на повну абстрактність елементів цієї системи: «Ми, — говорить він, — мислимо три різні системи речей: речі першої системи ми називаємо точками й позначаємо А, В, С…- речі другої системи ми називаємо прямими та позначаємо а, в, с…- речі третьої системи ми називаємо площинами і позначаємо» [2, 56].

Гілберт уводить різного роду відносини між елементами системи: «безперервність», «паралельність», «приналежність», «конкретність» або «співмірність». У них фіксуються абстрактні відносини, що належать до різних теоретичних систем. Така аксіоматична система стала більш ємною, синтетичною і широко застосовуваною до інтерпретацій різної предметної галузі. Аксіоматика Д. Гільберта будувалася на математичній логіціпринципи несуперечності, незалежності, повноти, можливості розв’язання, на відміну від конкретно змістовної аксіоматики, також доводяться, хоча на змістовному, семантичному рівні. Геометрія Евкліда стала однією з інтерпретацій, моделей геометрії Д. Гільберта. У цій геометричній системі зростає роль суворості доказів, розвиваються принципи інваріантості, ізоморфізму й відповідності. За допомогою теорії моделей установлюється зв’язок з емпірією.

Але з розвитком теоретико-множинних відносин виникають нові протиріччя. Так були викликані до життя старі парадокси типу «брехуна», «купи», «ідеї про ідею» — є нова «ідея». Ці парадокси сформульовані у вигляді парадоксів Рассела-Цермело, як множина усіх множин, що не містять себе як елементипарадокс Кантора про найбільше координальне числопарадокс Буралі-Форті, що належить до порядкових трансфінітних чисел та ін. Аналізуючи становище, яке виникло в основах математики, багато найвизначніших учених втратили впевненість. На теорію множин Кантора з усіх боків обрушилася різка критика. Зіштовхнувшись з парадоксами теорії множин, Фреге і Дедекінд фактично відмовилися від своїх точок зору і припинили подальшу роботу. Характеризуючи становище, що склалося, Д. Гільберт пише: «Треба погодитися, що стан, у якому ми перебуваємо нині щодо парадоксу, на тривалий час нестерпний. Подумайте: у математиці - цьому взірцеву достовірності та істинності, — утворення понять і хід умовиводів, як їх всякий вивчає, підносить і застосовує, проводять до безглуздя» [2, 349].

Усі парадокси, які виникли, говорили про те, що математичні теорії побудовані не на суворих підставах, необхідно було абстрактно змістовну аксіоматику замінити на більш сувору. Розробити таку логічну систему, де необхідно буде сформулювати самі поняття «доказ», «формула», «логічне правило», «логічний закон» і формалізувати не тільки аксіоматичну систему, але і правила висновку, тобто не тільки семантичну частину висновку, але й її синтаксис.

Така кодифікація і логічна побудова всієї теоретичної математики приводить до деякої єдиної логічної системи, де виконуються операції над формулами за суворо визначеними правилами. «Ця гра формулами здійснюється за певними цілком визначеними правилами, — говорить Гілберт, — у яких виражається техніка нашого мислення» [Там же, 382].

Отже, цей процес такої побудови кодифікує і систематизує наше мисленнямислення дослідника при побудові математичної теорії додержується законів правильного мислення. Така систематизація розумового апарату, з погляду Гільберта, приведе до суворої, безпомилкової побудови математичної теорії. «Ці правила утворюють замкнену систему, яку можна знайти й остаточно задати. Основна ідея моєї теорії доводу зводиться до опису діяльності нашого розуму, інакше кажучи, це протокол про правила, згідно з якими фактично діє наше мислення» [Там же].

Гільберт був глибоко переконаний в істинності своєї теорії доказу. Такою системою побудови він сподівався врятувати математичні теорії від парадоксів, очистити її від несуворостей у побудовах і одержати істинне знання в чистому вигляді.

Посилаючись на Аристотеля, Гільберт глибоко вірив у силу людського розуму, у те, що він здатний осягнути абсолютну істину. «Підтверджується те, — говорить він, — що, можливо, передчував уже Аристотель, а саме: що наш розум не проводить ніяких таємничих фокусів, а, навпаки, користується тільки цілком визначеними, встановленими правилами — що є разом з тим запорукою абсолютної об'єктивності його суджень» [Там же, 399]. Глибоко вірячи в ідею суворості дедуктивного доказу, Гільберт закликав до побудови такої логіко-дедуктивної теорії, яка б вивела математику з кризового становища. «Я вірю, — говорить ін, — що моя теорія доводу робить нам ще ширшу послугу. Адже що було б з істинністю наших знань взагалі і як склалося із здійсненням та прогресом науки, якби навіть у математиці не було достовірної істини?» [Там же].

Формальна аксіоматика зіграла помітну роль у становленні математичної теорії в її несуперечності. Найбільш повно проявилися методологічні принципи несуперечності, незалежності, повноти і проблема можливості розв’язання при аксіоматизації арифметики.

Але відповідь на запитання Гільберта про досягнення істинності, вірогідності і її доказу за допомогою цієї замкнутої формальної аксіоматичної системи не примусила себе чекати.

Аналізуючи формальні аксіоматичні системи, К. Гедель у 1931р., а потім С. Кліні довели обмежені можливості будь-якої формальної аксіоматичної системи. Теорема Геделя про несуперечність і повноту аксіоматичної системи дедуктивно довела, що, якщо система аксіом неповна, то вона несуперечлива, протиріччя настає, якщо вона стає повною. У будь-якій математичній теорії можуть бути сформульовані пропозиції, що неможливо ні довести, ні спростувати засобами цієї аксіоматичної системи, але, приєднуючи цю пропозицію аn+1 або її заперечення до даної аксіоматичної системи а1- а2- а3- аn, одержимо нові аксіоматичні системи. Уперше в історії математики таке розширення зробив Евклід, приєднавши до аксіоматики своєї геометрії 5-й постулат, і з «абсолютної геометрії» одержав геометрію Евкліда, а потім, більш ніж через 2000 років, застосувавши постулат, зворотний 5-му, Н.І.Лобачевський, К. Гаусс і Я. Боян побудували уявну, неевклідову геометрію.

Така побудова аксіоматичних систем має велике гносеологічне значення, стало можливим будувати різного роду аксіоматичні системи, що мають різного ступеня виражальні можливості і застосовності в різних галузях наукового знання. Формально аксіоматичні системи дали можливість поставити ряд філософських питань про співвідношення формального і змістовного в науковому пізнанні, про співвідношення точного й неточного в знанні, що розвивається, про алгоритмізацію, програмування й межі застосовності обчислювальних засобів в одержанні точного знання, про побудову розумових операцій і співвідношення предмета і пізнавальних можливостей за допомогою побудованих логічних структур і обчислювальних засобів. Уся ця логіко-дедуктивна аксіоматична система стала підготовчим етапом для побудови однієї з могутніх галузей сучасної математичної галузі - алгоритмізації, програмування й обчислювальних засобів, без яких немислимий сучасний науково-технічний прогрес. Розглянемо докладніше цей математичний напрямок.

Застосування різного роду обчислювальних засобів, побудова для них програм є невід'ємною частиною в розв’язанні сучасних науково-технічних, соціально-економічних, екологічних та інших задач. З огляду на важливість цих задач, що доводиться вирішувати за допомогою ЕОМ і програмування, природно виникає питання про надійність програмування й обчислювальних засобів.

Теоретичною основою побудови програм на ЕОМ, як було відзначено, стала «Програма Гільберта», його теорія доказу, за допомогою яких він зробив спробу повної формалізації математики.

Гільберт, як відомо, ставив перед собою завдання деталізації кожного кроку доказового мислення, його логічного обґрунтування, де піддавалися повній формалізації не тільки математичні теорії, але і правила висновку, він прагнув розробити такий метод, який би копіював закони правильного мислення.

У процесі розв’язання різного роду науково-технічних задач і формування наукового світогляду діє новий технічний феномен. Він сприяє реалізації розумової діяльності в тій мірі, у якій розумова діяльність здатна розчленовувати досліджуваний процес на елементарні операції. До цього прагнули за всіх часів математики, фіксуючи правила дій з ідеальними об'єктами, виконуючи різного роду логіко-математичні операції. Цей ланцюжок дій над ідеальними об'єктами являв собою ідеальний процес, що деякою мірою заміняв реально існуючий досліджуваний процес. Але спосіб мислення, у свою чергу, повинен відбивати реально існуючий досліджуваний процес. Дослідник прагне розгадати закономірності природи, вибираючи визначений шлях і метод дослідження, користуючись своїм світоглядом і результатами обчислювальних засобів. Дослідники і раніше використовували математичні методи, алгоритми. Але обчислювальні засоби (програмування, ЕОМ) не були розвинуті настільки, щоб можна було вибрати метод дослідження й аналізувати різні варіанти розв’язку. При цьому ставиться завдання можливості розв’язання того чи іншого питання за кінцеву кількість кроків. Це спрощує, деталізує процес, являє свого роду редукційний метод дослідження, в остаточному підсумку ставиться завдання можливості розв’язання.

" Прояснення поняття розв’язності даного математичного питання за кінцеве число кроків якраз і є одним із завдань, поставлених Гільбертом перед теорією математичного доводу в його доповіді «Аксіоматичне мислення» [3, 505]. «Програма Гільберта», як відомо, була породжена боротьбою різних математичних і філософських шкіл з формалізмом, логіцизмом, інтуїціонізмом. Ця боротьба ідей привела до розвитку конструктивізму в математиці і різного роду логічних числень.

У кожен історичний період розвитку наукового знання виникає свій певний стиль мислення. Так і в наш час, у період науково-технічного прогресу, переважає кібернетичний стиль мислення. Це, у свою чергу, породжує такі канонізовані уявлення сучасного стилю наукового мислення, як принципи моделювання, ідею математичного світу й спільності конструктивно-технологічного підходу.

У період науково-технічного прогресу створені нові обчислювальні засоби. Кібернетика стає основою системи управління. Кібернетичний стиль мислення, мова кібернетики стали загальнонауковими. Кібернетика впливає на розвиток природничо-наукових, технічних дисциплін, проникає в питання мовознавства й інші суспільні науки. «Роль кібернетики як парадигми сьогодні виражається і в тому, що вона значною мірою впливає на формування мови сучасного природознавства, його концептуально-понятійний апарат» [4, 4]. У цьому плані кібернетика, її мова сприяють розвитку приватних наук, вони являють собою основну структуру приватно наукового знання, установлюють певну послідовність і систему його побудови. Але ці побудови повинні мати суворо науковий, доказовий характер.

Протягом тисячоліть, починаючи зі Стародавньої Греції, найбільш міцну основу істинного мислення знайшов дедуктивний доказ. Але історичну тенденцію дедуктивного обґрунтування необхідно обернути на модерністський спосіб «добування» нового знання за допомогою ЕОМ. Загальновідомо, що ЕОМ може розв’язувати не тільки практичні задачі, але й вирішувати проблематику найбільш абстрактних галузей, зокрема доказ математичних теорем. При цьому слід зазначити, що ЕОМ не може порушити фундаментальних принципів дедуктивного доказу (несуперечності, повноти і незалежності). Але машинний доказ теорем не має міцного обґрунтування, він базується на так званій емпіричній основі, експериментальних оцінках і емпіричних узагальненнях. Однак практична ефективність і «модність» роботи ЕОМ відтінює як другорядне дедуктивне обґрунтування роботи самої ЕОМ.

Поява надпотужних ЕОМ поставила перед дослідниками два основних завдання, відзначає Е. Дейкстра:

застосовність цих машин до розв’язання таких задач, які б себе виправдали;

але якщо ці машини представляють більш могутні обчислювальні засоби, то зростають і запити суспільства до вирішення різних більш складних і інтелектуальних сфер застосування [5, 267].

Як відомо, будь-яка наука повинна мати певні «розміри», повинна бути «доступною для огляду», її інформативні можливості людина повинна засвоїти і не втрачати їх при подальшому вивченні. Ще слід зазначити, що кожен розділ людського знання повинен бути певним чином відокремленим від інших наукових дисциплін. Аналогічні вимоги варто застосувати і при побудові програм для ЕОМ. «Така аналогія побудови наукового знання при побудові програм для ЕОМ, — відзначає Є. Дейкстра, — приводить до постановки тих же задач «розміру та різноманітності» [Там же], тобто розміру програми й різмаїтості розв’язуваних задач. Але для глибокого осмислення сутності деякого процесу необхідні її деталізація, розбивки, розчленовування на частини.

Важливо вибрати ізольований аспект. «Головна характерна риса культурного мислення, на мою думку, — відзначає Є. Дейкстра, — полягає в тому, що людина може і хоче глибоко вивчити певний аспект ізольовано, заради його власного змісту, усвідомлюючи у той же час, що вона займається тільки одним з аспектів. Інші аспекти мають чекати своєї черги, тому що наші голови такі малі, що не можуть без плутанини працювати з усіма аспектами одночасно» [Там же]. Така постановка питання цілком погоджується з діалектичним методом пізнання, уточнення абсолютно істинного знання.

Для заглиблення в сутність речей більш високого порядку «важливе значення має правильність складання програм, подавання їх в такому вигляді, щоб можна було встановити їх істинність, при цьому … можна загорітися бажанням аксіоматизувати якомога універсальнішу мову програмування або обережно знайти найефективніші обмеження» [Там же, 270].

Але як піддати повній аксіоматизації й наступній формалізації яку-небудь задачу? Адже вона може складатися з різних математичних розділів, і її математичне забезпечення може бути різнорідним. Неможливо за допомогою однієї аксіоматичної системи скласти математичне забезпечення для вирішення даної програми. У такому випадку неможливе єдине дедуктивне обґрунтування всієї програми. Різні задачі мають і різну структуру побудови, і ступінь формалізації. При цьому необхідно домагатися максимальної простоти розумно керованих програм. Зважаючи на те, що в даний час програмування стало загальноприйнятим «ремеслом» у розв’язанні різного роду наукових і народно-господарських завдань, то слід це «ремесло» поставити на наукову основу і навчитися обґрунтовано складати програми, представляти це як певну логіко-математичну конструкцію. У процесі побудови програми необхідне її поетапне обґрунтування, обґрунтування кожної її формалізованої частини. Що ж стосується всієї програми, то критерієм істинності повинне бути її практичне обґрунтування.

У програмуванні на ЕОМ спостерігається дві тенденції. Одна з них являє розробку формалізованих алгоритмічних систем, тобто теоретичний напрямок у розвитку програмування. Цей теоретичний напрямок являє собою одну з форм побудови конструктивної машинної математики, інший напрямок являє собою еволюцію експериментальних програм, які можна розглядати як одну з форм індуктивного напрямку в розвитку машинної математики. Діалектична взаємодія індуктивних і дедуктивних методів у побудові машинної математики повинна мати загальне методологічне обґрунтування в правильності побудови програм ЕОМ.

Така еволюція у взаємодії індуктивних і дедуктивних методів, мабуть, у майбутньому повинна привести до створення так званих «гібридних» програмованих систем, вести в бік їхнього узагальнення й універсалізації. «Еволюція як „інтелектуальних“ пакетів програм, — відзначає І. Н. Молчанов, — так і експертних систем у майбутньому, очевидно, приведе до створення гібридних систем, у яких використовуватимуться як формалізовані алгоритми обробки інформації, так і досвід спеціалістів-операторів. Саме в гібридних експертних системах поєднуватимуться як „жорсткі“, так і „м'які“ моделі та способи обробки інформації» [6, 58].

Цікаві надії плекає Р. Андерсон: «Якби можна було формалізувати довід правильності та проводити його абсолютно надійним взірцем (як автоматично доказовим пристроєм), то йому можна було б повністю довіряти. У майбутньому це, можливо, виявиться реальним, але не зараз» [7, 26].

Проаналізуємо ряд аспектів неможливості повного дедуктивного обґрунтування сучасних програм ЕОМ. Як відомо з теорем К. Геделя про неповноту логічних систем, неможлива повна формалізація жодної змістовної теорії. Якщо програма для ЕОМ буде побудована аксіоматично і буде розпочата спроба її формально-логічної побудови, то це завдання виявиться теоретично нездійсненним. А якщо врахувати, що жодна програма не може бути побудована за допомогою однієї аксіоматичної системи, то питання повної її формалізації відпадає. Крім цього, в процесі побудови формалізмів можуть бути пропущені логічні помилки, які важко з’ясовуються і які приведуть до побудови неправильних програм. Історичним прикладом такої помилки може служити теорема Х. Ербрана, доведена ним у 1930 р., на якій засновані найбільш розповсюджені машинні алгоритми. За допомогою цих алгоритмів здійснюється пошук доказів теорем математичної логіки. Ця важкоусувна помилка була виявлена тільки в 1963 р. Такого роду помилки в логічних побудовах програм ЕОМ можуть спостерігатися й в інших випадках. Їх можна усунути в результаті застосування іншого логіко-математичного апарату в процесі розвитку науки або практичної перевірки програм. «Але програма щодо доказу правильності програм, — відзначає А. І. Анісімов, — у свою чергу, має потребу в доводі правильності. Очевидно, в кінцевому підсумку правильність версифікуючої програми має бути доведена людиною» [8, 38]. Ієрархічна побудова програм для обґрунтування попередньої програми являє собою свого роду метапрограми різних рівнів. Для встановлення істинності попередньої програми, очевидне питання не теорії, а чисто практичне питання, людська практика повинна підтвердити істинність теоретичних висновків програмування.

Слід зазначити, що зростання, розвиток математичної науки приводить до розвитку нових форм дедуктивного обґрунтування програм, це також підтверджує неможливість побудови єдино правильної і дедуктивно обґрунтованої програми ЕОМ.

При побудові програми важливим фактором є високий професіоналізм як у вивченні задачі, яку необхідно розв’язати, так і в самому логіко-математичному забезпеченні. З огляду на професійні труднощі, у наш час наукова думка спрямована на спеціалізацію і створення персональних ЕОМ — ПЕОМ. Персональні ЕОМ сприяють більш глибокому вивченню предметної галузі, тобто вивченню сутності речей. «Створений фахівцями у даній предметній галузі програмний продукт формалізує такі його тонкощі, які, по-перше, не вкладаються у традиційні моделі, по-друге, недоступні професіональним програмістам-виготовлювачам тиражованих пакетів прикладних програм» [9, 4].

Як бачимо, подібні програми точніше характеризують предметну галузь. В основу алгоритму покладений принцип максимального задоволення потреб користувачів ПЕОМ, визначення набору типових функцій для кожної галузі і вимог, що ставляться з боку споживача конкретної галузі до ПЕОМ. Такого роду спеціалізація обчислювальної техніки і її програм сприяє проникненню в сутність речей, більш глибокому їхньому вивченню, але недоліком їх є їхній приватний характер. Очевидно, подальший розвиток обчислювальної техніки повинен враховувати і такий персональний спеціалізований напрямок.

Але як би детально не вивчалася предметна галузь, неможливо цілком запрограмувати будь-який процес, створити програму, яка встановлює загальний універсальний зв’язок того чи іншого процесу або явища. Програма тільки в грубій, наближеній формі може його характеризувати. Але й не тільки в цьому може бути причина неточності програм. При перевірці правильності складання програми на машині машина може давати «збої» у перевірці. Це утруднить перевірку правильності її побудови. Іншим «бар'єром» у правильності побудови програм є обмежені можливості суб'єкта, укладача програм.

Ще при виділенні визначеної задачі необхідно визначити поняття практичної видимості чи неозорості математичного твердження. Якщо математична задача зводиться до неозорої процедури, то важко гарантувати її істинність при побудові програм. У цьому випадку набирає сили діалектика кінцевого і нескінченного. «Неосяжна процедура, яка реалізується в істотній частині ЕОМ або допускає редукцію до досяжного доводу методами, які є у розпорядженні математиків» [10, 31]. Дійсно, кожен неозорий процес може бути помилковим, але ця помилка може бути виявлена при подальшій розробці і перевірці програм, розробці математичного забезпечення. В остаточному підсумку неможливо формалізувати цілком жоден процес. Справедливо зауважує Ю.І.Манін, що математичний світ має певну реальність і внутрішнє життя, що мало залежить від формалізмів, покликаних його описувати.

Ще слід зазначити могутні інтегративні властивості програмування й ЕОМ у науковому пізнанні. Програмування, машинна математика стали новим напрямком у науковому пізнанні. Вони сприяють проникненню в різні галузі людського знання, вони «стерли» грані між гуманітарними і природничо-науковими дисциплінами. Усі науки стали математизуватися за допомогою нової машинної математики, що дало новий імпульс у розвитку сучасного наукового знання.

Розглядаючи програмування як принципово новий метод у науковому пізнанні, академік В. М. Глушков відзначає, що цей математичний експеримент «займає проміжне місце між класичним дедуктивним методом і класичним експериментальним методом дослідження» [10, 32]. У зв’язку з цим можна говорити про новий напрямок у розвитку математики, який базується й на математичному формалізмі, й на здоровому глузді, що дозволяє зближати математику з експериментальними науками (природознавством, економікою та ін.). «У ХХ столітті математика перетворилась у своєрідну індустрію концептуальних систем будь-якої міри спільності, репрезентативної сили, інформаційної ємності, прогностичної могутності, пояснювального потенціалу» [11, 160]. Це сприяє збагаченню і розвитку як математики, так і математизованих наук. Вивчаючи дослідницькі можливості машинної математики, багато вчених схильні вважати, що вся історія розвитку математики є передісторією сучасної математики, що бурхливо розвивається, і має велике майбутнє як у розвитку самої математики, так і в математизації всього наукового знання.

ЛІТЕРАТУРА:

1. 1.Аристотель. Соч. в 4-х т. — Т.2. — М.: Мысль, 1978. — 687 с.

2. 2.Гильберт Д. Основы геометрии. М. — Л. ОГИЗ, 1948. — 491 с.

3. 3.Гильберт Д., Бернайс П. Основания математики, теория доказательств. — М.: Наука, 1982.

4. 4.Свинцицкий В. Н. Кибернетический стиль мышления в современном научном мире //Философ. проблемы соврем. Естествознания. — No 47. — 1979.

5. 5.Дейкстра Э. Дисциплина программирования. — М.: Мир, 1978.

6. 6.Молчанов И. Н. Проблемы и перспективы развития прикладного программного обеспечения //Управляющие системы и машины. — No2. — 1988.

7. 7.Андерсон Р. Доказательство правильности программ. — М.: Мир, 1982.

8. 8.Анисимов А. М. ЭВМ и понимание математических доказательств //Вопр. философии. — No 3. — 1988.

9. 9.Яковлев Ю. С., Новиков Б. В., Штерн Ю. М. и др. Принципы организации инструментальных средств автоматизации прикладного программирования для персональных ЭВМ //Управляющие системы и машины. — No 2. — 1988.

10. 10.Глушков В. М. Соч. Т.2.

11. 11.Философский анализ особенностей развития современного естествознания. — Киев.: Наукова думка, 1984.