Размещено на http://www.allbest.ru/

Харківський національний університет радіоелектроніки

Гуца Олег Миколайович

УДК 519.711: 681.3/06

Інтерактивна модель перекладу технічних завдань у систему булевих формул

АВТОРЕФЕРАТ

дисертації на здобуття наукового ступеня кандидата технічних наук

01.05.02 - математичне моделювання та обчислювальні методи

Харків - 2002

Дисертацією є рукопис.

Робота виконана у Харківському національному університеті радіоелектроніки, Міністерство освіти і науки України.

Науковий керівник кандидат технічних наук, доцент Матейченко Віктор Валентинович, Харківський національний університет радіоелектроніки, доцент кафедри електронних обчислювальних машин.

Робота присвячена проблемі спілкування людини з машиною в умовах значного збільшення числа як користувачів, так і обслуговуючих їх засобів автоматизованої обробки інформації, в першу чергу персональних ЕОМ (ПЕОМ).

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

Існуючі процедури формалізації СО, наприклад, технологічних процесів (ТП) дорого коштують, багатоступінчасті і тому практично недосяжні для кінцевого користувача (КК) ПЕОМ. У роботі пропонується модель та реалізуюча її програма формалізації СО. Результатом роботи програми для конкретного ТЗ або складаючих його часткових ТЗ (ЧТЗ) - є система булевих формул (СБФ), що створена не як задача синтезу кінцевих автоматів, а внаслідок розв'язання задачи “перекладу” СО на мову булевої алгебри. Даний підхід розглянутий також у проблемі визначення та створення нових інформаційних технологій (НІТ). НІТ як поняття є результатом удосконалення процесів людино-машинного спілкування, в ході развитку яких до неї сформувалися певні вимоги. Користувач ПЕОМ, спираючись на результати НІТ, отримані в даній роботі, має змогу самостійно оперувати з поняттями власної предметної галузі, визначаючи в ній окремі об'єкти та зв'язки.

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

Зв'язок роботи з науковими програмами, планами, темами. Дисертаційна робота виконана відповідно з планами науково - господарчих робіт Харківського національного університету радіоелектроніки у межах держбюджетної теми №522: “Розробка учбово-методичного забезпечення та програмно-апаратних методів для нових учбових дисциплін з комп'ютерних наук та комп'ютерної інженерії”, включеної в координаційний план Міністерства освіти і науки України (№ ДР 0197U012176), де автор запропонував використати свою модель “текст смисл” для формалізації ТЗ і темі № 102 “Розробка основ нових інформаційних технологій у автоматизації проектування, методів діагностики радіоелектронної апаратури та ОТ” (№ ДР 0100U003417), де автором запропонований концептуально-технологічний підхід до створення НІТ (включаючи комп'ютерні НІТ).

Мета та завдання дослідження. Метою дослідження є розв'язання задачі перетворення СО алгоритмів управління ТП до СБФ.

Досягнення даної мети полягає у проробці наступних часткових задач:

- визначення предметної області;

- аналізу існуючих засобів формалізації (у вигляді булевих формул);

- вибору моделі формалізації;

- реалізації і оптимізації обраного методу синтезу моделі;

- верифікації отриманих результатів.

Об'єктом дослідження є інтерактивний процес людино-машинного перетворення СО алгоритмів керування ТП у СБФ.

Предметом дослідження виступає мова-посередник, як засіб формалізації СО.

Методи дослідження. В роботі використані наступні методи: математичної лінгвістики (при доборі моделі та предметної області), зчислення висловлювань (при переході до математичної моделі), математичної логіки (при побудові обмежень), булевої алгебри (при доведенні тверджень), теорії множин (при формуванні рішень), системотехніки (при розв'язанні прикладних задач), програмування та оптимізації (при розробці пакету прикладних програм).

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

У роботі використано еквівалентні методи перетворення і оптимізації математичних моделей і нетрадиційну для задач логічного синтезу модель “текст смисл”, що відповідає п.1 підр. 1.1 (напрямок досліджень) паспорту спеціальності.

Показано ефективне використання методів обчислювальної математики, яке враховує особливості реальних технологічних задач і забезпечує створення ефективних програмних засобів комп'ютерної реалізації. Це відповідає пункту 2 підр.1.1 паспорту спеціальності.

Розроблено:

- програмну систему моделювання, включаючи структурну, алгоритмічну організацію та інформаційну технологію, що відповідає п.3 підр.1.1 паспорту спеціальності;

- новий метод організації і оптимізації процесу моделювання, в тому числі підготовку початкової інформації, її перетворення і верифікація, що відповідає п.4 підр.1.1 паспорту спеціальності.

Наукова новизна отриманих результатів полягає в тому, що по ходу рішення наведених вище задач автором було:

- вперше здійснено вибір моделі для досягнення мети з використанням раніше відомої моделі "смисл текст" (що використовувалася для розв'язання задач перекладу з однієї природньої мови на іншу);

- отримав подальшого розвитку концептуально-технологічний підхід до подання результатів дослідження у межах даного підходу;

- вперше реалізовано та описано у природньо-мовній та програмній формах алгоритм переходу від мови-посередика (умовних секвенцій) до СБФ;

- вперше розв'язано варіант аналогічної задачі для автоматів управління із зосередженою пам'яттю;

- вперше поставлено і розв'язано задачу оптимізації системи умовних секвенцій (СУС) при обмеженнях з використанням принципу еквівалентування;

- вперше розроблений метод верифікації СУС.

Практичне значення отриманих результатів полягає у можливості їх безпосереднього застосування у складі системи прикладного програмного забезпечення персональних комп'ютерів. Одна з програм (SEQVEN) введена до складу бібліотек прикладних програм кафедри ЕОМ та навчального обчислювального центру ХНУРЕ.

Результати дослідження викладаються у трьох лекціях та двох лабораторних роботах кафедральної дисципліни "Основи автоматизованого проектування засобів обчислювальної техніки".

Під час роботи на Харківському приладобудівному заводі ім. Т.Г. Шевченка окремі результати дослідження були впроваджені у розробки ОКБ заводу.

Особистий внесок здобувача. Основні результати були отримані здобувачем самостійно. У роботах, написаних із співавторами, здобувачу належить: [54] - розроблено метод перетворення СО у секвенціальний опис (СкО), надано визначення перемінної із пам'яттю, сформульовано вимоги для одержання коректного СкО пристроїв із пам'яттю; у [55] - відповідно запропонованому ТП керування пранням білизни у пральні складено СкО та отримана відповідна СБФ; у [56] - запропоновано застосування мови умовних секвенцій як мови-посередника для формалізації СО; у [ 57] - визначена парна структура причинно-слідчих зв'язків СО, що підлягають еквівалентизації, та знайдено рішення задачі еквівалентизації в умовах повного перебору складових частин умовних секвенцій; у [93] - розроблено керуючий автомат процесора Петрі.

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

Апробація результатів дисертації проводилася на засіданнях кафедри ЕОМ ХНУРЕ, професорсько-викладацьких конференціях факультету ОТ (КІУ) ХНУРЕ, матеріалах “Школы проектирования автоматизированных систем контроля и управления сложными объектами” Харків - Туапсе (1992); були оголошені у вигляді доповідей матеріали "Эквивалентные преобразования системы условных секвенций", а також "Проектирование дискретных устройств при ограничениях на тип памяти" на науково-технічній конференції "Техника и физика электронных систем и устройств" м. Суми (1995); робота обговорювалася на поширеному засіданні трьох кафедр факультету КІУ ХНУРЕ (прот. каф. ЕОМ ХНУРЕ №1 от 01.09.2001 р.).

Публікації. Результати наукових досліджень відображені у 9 друкованих працях. До них входять 4 статті, опубліковані у наукових виданнях, що включені у Перелік ВАК України, а також тези 4 доповідей та авторське свідоцтво.

ОСНОВНИЙ ЗМІСТ РОБОТИ

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

Розділ 1. Проведено огляд літератури і визначені задачі дослідження, що підлягають розробці. Виходячи з огляду, такими задачами є: добір моделі формалізації предметної області, аналіз існуючих засобів формалізації (в сенсі отримання системи булевих формул), реалізація і оптимізація обраного методу синтезу моделі, верифікація отриманих результатів.

Розділ 2. У розділі наводяться результати розробки: моделі предметної області, на основі якої проводяться подальші дослідження і пропонується методика концептуально - технологічного підходу як методичної основи роботи. Предметна область (ПрО) обмежена технологічними процесами ТП, тому задачею користувача є швидко “навчити” ПЕОМ виконанню такого корисного перетворення інформації, яке раніше виконувалося людиною самостійно. Прототипом моделі є лінгвістико-математична модель "смисл текст".

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

Концептуально-технологічний підхід до розробки сформувався у вигляді інтегрального поняття НІТ, що містить в собі елементи нового підходу до виробництва, засобу одержання продукту новими шляхами, методами і ресурсами.

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

Дається (вибірково) огляд існуючих методів формалізації алгоритмів управління ТП: графічні - граф-схеми алгоритмів, часові діаграми; табличні - таблиці істинності, карти Карно, таблиці переходів, матриці переходів, мовно - логічні схеми алгоритмів. Розглядається формалізація задач з використанням концептуально-технологічного підходу: графічний метод - сітки Петрі і мови, засновані на зчисленнях висловлювань, а також формалізація у продукційних системах, тобто мов, що використовують різновид продукцій - мова секвенцій (МС) та мова умовних секвенцій (МУС). При використанні МС кожна складова частина логічного висловлювання має вигляд “якщо f(x)=1, то g(y)=l”.

Вимоги до мови - посередника СО можна сформулювати наступним чином: а) бажано, щоб мова описання алгоритмів була єдиною як для автоматів “з пам'яттю”, так і для автоматів “без пам'яті”; б) доцільно ще більше наблизити структуру цієї проміжної мови до СО, тобто задавати програму роботи не у вигляді ДНФ, а більш дрібними частками; в) слід передбачити правила, що зводять до мінімуму можливі протиріччя у описанні на цій мові. Кінцевою метою в цьому напрямі є створення формалізованої мови, яка б дозволяла за словесним описанням (під диктовку) записувати часткові логічні умови і коректно об'єднувати їх у формули. Викладеним вимогам відповідає мова умовних секвенцій.

Розділ 4. Перехід від СО моделі до СБФ можна поділити на наступні основні етапи: а) складання СУС; б) верифікація СУС; в) мінімізація СУС; г) трасформація СУС у СБФ. Розглянемо перший та останній з наведених етапів. Спочатку складається список вхідних, вихідних та внутрішних змінних, після чого записується СУС, використовуючи 4 оператори: "ПОЧАТОК", "ПРОГРАМА", "АЛЕ" і "КІНЕЦЬ". Кожен з операторів, крім останнього, є початковим відповідного блоку в СУС.

Перехід до СБФ відбувається за чотирма правилами:

а) для кожної вихідної змінної, що має початкове значення Y_i = 0, логічно скласти ліві частини тих УС, до правих частин яких вона входить без інверсії;

б) отриману логічну суму треба логічно помножити на добутки інверсій лівих частин тих УС, до правих частин яких вихідна змінна Y_i входить з інверсією;

в) для вихідних змінних з початковим значенням Y_i = 1 записати тільки логічний добуток інверсій лівих частин УС, до правих частин яких вихідна змінна Y_i входить з інверсією;

г) якщо у СУС є оператор "АЛЕ", то для кожної вихідної змінної до формули, отриманої з УС, записаних до оператора "АЛЕ", логічно додаються формули, отримані з УС, записаних після цього оператора.

У розділі розглянуто також задачу визначення типу елементу пам'яті з його секвенціального описання (СкО), що проводиться у кілька етапів.

Розділ 5. СУС, складена згідно з вимогами, наведеними у попередньому розділі, містить у собі надлишкову кількість УС. У той же час, виходячи з правил перетворення, мінімальність початкової СУС є одним з основних критеріїв оптимальності СБФ.

Мінімізація СУС - це процедура отримання системи мінімальної складності з початкової розподіленої СУС (СУСР) при заданому наборі спрощуючих правил (що мають назву тверджень). Процедура виконується щляхом попарного порівняння усіх УС, що входять до СУСР. Пошук проводився на повному наборі можливих варіантів і полягає у виконанні: а) перетворенні СУСР у БФ за наведеними вище правилами; б) мінімізації БФ табличним методом; в) зворотному перетворенні БФ у СУСР; г) співставленні початкової та отриманої СУСР для оцінки результатів мінімізації; д) об'єднанні еквівалентних форм за групами у залежності від схожості результатів. Виявилося, що 67% комбінацій призвело до зменшення числа УС або змінних у УС. Отримана множина еквівалентних форм була поділена на 10 груп, у яких мінімізація можлива при виконанні певних умов.

Умови мінімізації викладені як твердження.

Твердження 1: Якщо у СУС є дві однакових УС, то одна з них із СУС виключається.

Твердження 2: Якщо у СУС є пара УС, до правих частин яких вихідна змінна входить з інверсним значенням, а ліві частини взаємно інверсні за наявністю спільної змінної, то із СУС (до оператора "АЛЕ") видаляються всі УС.

Твердження 3: якщо у СУС є пара УС, у праві частини яких вихідна змінна входить з прямим значенням, а ліві частини утворюють взаємну інверсію спільної змінної, то із СУС (до оператора "АЛЕ") виключаються усі УС з прямим значенням вихідної змінної у правій частині.

Твердження 4: якщо у СУС є пара УС, у праві частини яких вихідна змінна входить зі взаємоінверсними значеннями, а ліві частини є взаємною інверсією спільної змінної, то із СУС (до оператора "АЛЕ") виключаються всі УС з прямим значенням вихідної змінної у правій частині.

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

Твердження 6: якщо у СУС є пара УС, у праві частини яких вихідна змінна входить зі взаємоінверсними значеннями і при цьому ліві частини УС містять спільну взаємоінверсну змінну, то із СУС виключається УС з інверсним значенням вихідної змінної у правій частині.

Твердження 7: якщо у СУС існує пара УС, в праві частини яких вихідна змінна входить з однаковими значеннями, а ліві частини відрізняються лише однією парою взаємоінверсних змінних (або однією змінною), то дана пара УС замінюється УС, ліва частина якої - це спільна частина лівих частин видалених УС.

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

Твердження 9: якщо у СУС є пара УС, до правих частин яких вихідна змінна входить з однаковими значеннями і при цьому ліва частина УС1 є підмножиною лівої частини УС2, відрізняючись лише полярністю однієї змінної, то із лівої частини УС2 дана змінна виключається.

Твердження 10: якщо у СУС є пара УС, до правих частин яких вихідна змінна входить з взаємоінверсними значеннями і при цьому ліва частина УС1 (з від'ємним значенням вихідної змінної у правій частині) містить тільки одну змінну, яка взаємоінверсна одній з підмножини змінних у лівій частині УС2 (з прямим значенням вихідної змінної у правій частині), то із лівої частини УС2 дана змінна видаляється.

СБФ, отримані з СУС після мінімізації, співпадають з СБФ, що мінімізовані традиційними методами.

Розділ 6. При верифікації, стосовно предметної області (ТП), задача поділяється на дві:

а) верифікація СУС, перевіряюча її відповідність СО. Вона у свою чергу поділена на природньомовну, тобто лінгвістичну частину встановлення еквівалентності на рівні смислу (див. розділ 3), та другу частину, здійснюючої перевірку повноти описання складеної користувачем СУС на підставі технічного завдання. Саме на цій фазі верифікації СУС може поповнюватися (див. розділ 4);

б) верифікація СБФ, що перевіряє еквівалентність складеної СБФ (тобто цифрового автомату СУС).

Задача а) допомагає перевірити СУС, задача б) - перевірити відповідність СБФ заданому СО, тобто перевірці алгоритму, якого потребує ТП.

У багатьох випадках складену СУС не можна безпосередньо переписати у вигляді програми, оскільки СУС треба структуризувати - при записі УС до СУС їхній порядок не впливає на СБФ. Для верифікації СУС порядок розміщення УС має істотне значення. Воно особливо важливе при наявності змінних з пам'яттю. Для розв'язання цієї задачі використовується двохступененева схема моделювання (моделювання з розподіленими змінними).

У загальному випадку структура програми, що моделює систему умовних секвенцій, матиме вигляд.

Описання, складене на МУС, може бути промодельоване на будь-якій мові програмування без використання спеціалізованих програм моделювання.

Верифікацію на мережах Петрі слід проводити для СБФ, переведеної у граф Петрі, що значно спрощує процедуру верифікації.

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

Описання програм. а) Програмний продукт “SEQVEN” написаний на мові програмування Object Pascal і призначений для: вводу СкО, мінімізації СкО, перетворення СкО у СБФ. б) Програмний продукт "WINPET" написаний на мові Pascal у середовищі Delphi з метою обробки поширених узагальнених мереж Петрі. У даній роботі він використаний як засіб верифікації системи булевих формул.

ВИСНОВКИ

Для її рішення був використаний метод моделювання (модель “текст смисл”). Отримано алгоритм і його програмну реалізацію, що дає можливість кінцевому користувачу формалізувати словесні описи.

Як результати дослідження пропонуються наступні висновки:

1. Відповідно до поставленої цілі дослідження модифікована існуюча лінгвістична модель “текс смисл”, що дало можливість зв'язати природномовний і аналітичний методи уявлення технічної інформації.

2. Як предметну область розглянуто словесні описи алгоритмів керування технологічними процесами у формі виявлення причинно-наслідкових зв'язків.

3. Проаналізовано існуючі засоби формалізації. Встановлено, що найбільш придатним для реалізації модифікованої моделі є мова умовних секвенцій ( як підмножина класу продукційних мов).

4. Запропоновано 4 правила перетворення секвенціального опису у систему булевих формул.

5. Проведено аналіз і запропоновано метод оптимізації на рівні секвенціального опису, для чого розглянуті і доведені 10 тверджень про еквівалентність.

6. Розроблено метод автоматичного визначення типу елемента пам'яті за його секвенціальним описом.

7. Розроблена двоетапна процедура верифікації, що дозволяє верифікувати як вихідний секвенціальний опис, так і отриманий результат - систему булевих формул.

8. Розроблено програмне забезпечення, що дозволяє кінцевому користувачу вирішити на ПЕОМ задачу перетворення словесних описів алгоритмів керування технологічними процесами у систему булевих формул, тобто одержувати “смисл” або “істину” у вигляді булевих формул із “тексту”.

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

СПИСОК ОПУБЛІКОВАНИХ РОБІТ ЗА ТЕМОЮ ДИСЕРТАЦІЇ

1. Гуца О.Н. Генерация проектных заданий // Інформаційно-керуючі системи на залізничному транспорті. - 1998. - №6. - С. 34-38.

2. Гуца О.Н. Верификация системы условных секвенций // Інформаційно - керуючі системи на залізничному транспорті. - 1999. - №1.- С.28-31.

3. Гуца О.Н. О связи научного поиска с новой информационной технологией // Вестник национального технического университета “Харьковский политехнический институт”: Зб. науч. тр. - Харьков: типография ХВУ, 2001. - С.23-26.

4. Гуца О.Н., Матейченко В.В. О преобразовании знаний пользователя в декларативную форму представления знаний // Інформаційно-керуючі системи на залізничному транспорті. - 2000. - №1. - С. 57-61.

5. Гуца О.Н., Матейченко В.В. Об использовании в САПР устройств управления языка условных секвенций // Материалы школы проектирования автоматизированных систем контроля и управления сложными объектами. - Харьков-Туапсе. - 1992. - С. 19

6. Гуца О.Н. Проектирование дискретных устройств с применением условных секвенций при ограничениях на тип памяти // Материалы научно-технологической конференции "Техника и физика электронных систем и устройств". - Сумы. - 1995. - Т. 1. - С. 46-47.

7. Гуца О.Н., Матейченко В.В. Алгоритмизация технических заданий, использующая подкласс продукций // Харьк. техн. ун-т. радиоэлектроники. Харьков, 1995. 9 с. Деп. в ГНТБ Украины 23.05.95, N 1242 - Ук95.

8. Гуца О.Н., Матейченко В.В. Эквивалентные преобразования системы условных секвенций // Материалы научно-технологической конференции "Техника и физика электронных систем и устройств". - Сумы. - 1995. - Т. 1.

9. Пат. 15213 А Україна, МКИ G06F15/20. Процесор Петрі / Гуца О.М., Запорожцев С.Ю., Калінін Г.О., Маркін О.М., Матейченко В.В. (Україна); ХНУРЕ. - № 93007088; Заявл. 21.12.93; Опубл. 30.06.97; Бюл. № 3. - 4 с.

АНОТАЦІЯ

Гуца О. М. Інтерактивна модель перекладу технічних завдань у систему булевих формул. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 01.05.02 - математичне моделювання та обчислювальні методи. - Харківський національний університет радіоелектроніки, Харків, 2002.

Розв'язано задачу породження системи булевих формул безпосередньо з тексту технічного завдання з допомогою ПЕОМ. Була використана запропонована модель "текст > смисл". Доведено 10 тверджень, на підставі яких складена програма, що дає змогу кінцевому користувачеві ПЕОМ у інтерактивному режимі отримати результат для керування його технологічними процесами. Саме на кінцевих користувачів ПЕОМ зорієнтовано дане дослідження, бо воно дозволяє їм розв'язувати практичні завдання, виходячи з словесно описаних моделей управління технологічними процесами, в тому числі з допомогою розробленої автором програми. Зроблена спроба перевірки дослідження вимогам розробленого концептуально-технологічного підходу до створення нових інформативних технологій. Автор сподівається, що роботу можна розглядати як спробу створення системи, заснованої на знаннях, а не на застарілому принципі "аби вийшло".

Ключові слова: система, булеві формули, технічне завдання, продукція, Пост, умовні секвенції, переклад, природня, проміжна, штучна мова, твердження, верифікація.

АННОТАЦИЯ

Гуца О. Н. Интерактивная модель перевода технических заданий в систему булевых формул. - Рукопись.

Диссертация на соискание ученой степени кандидата технических наук по специальности 01.05.02 - математическое моделирование и вычислительные методы. - Харьковский национальный университет радиоэлектроники, Харьков, 2002.

Работа над указанной темой была инициирована парадигмой "конечный пользователь ПЭВМ и технолог производства в одном лице", что налагает ограничения на степень его информированности о вычислительных науках.

В ходе разработки были определены концепция конечного пользователя ПЭВМ с одной стороны и предметная область (технические задания) как подмножества естественно-языковых описаний - с другой. Это дало направление для поиска прототипа модели (математико-лингвистической) и цели математико-логической. Поэтому в качестве прототипа была выбрана известная модель "смысл текст" (перевод с языка на язык) и в качестве цели - получение системы булевых формул. В работе используется предложенная мною модель "текст смысл" как точно отвечающая поставленной задаче. В качестве аппарата формальных преобразований был выбран продукционный метод как наиболее соответствующий прагматическому (интуиционистскому) пониманию языка конечным пользователем ПЭВМ с одной стороны и допускающий его логическую обработку на ПЭВМ с другой. Большое значение в работе играет промежуточный импликационный язык условных секвенций. Этот язык требует от разработчика нахождения причинно-следственной связи между входными сигналами и требуемой реакцией на них со стороны компьютера (логическое управление).

В работе уделено значительное место задаче оптимизации (раздел 5). Поставлено и доказано 10 утверждений, на основе которых составлена программа, давшая возможность конечному пользователю ПЭВМ в интерактивном режиме получить оптимальный результат для управления его технологичекими процессами.

Разработан метод автоматического определения типа элемента памяти по его секвенциальному описанию.

Поставлена, решена и опубликована задача методической оценки законченности исследования с помощью концептуально-технологического подхода в виде последовательности "концепция принципы методы алгоритмы программы новые информационные и компъютерные технологии".

Разработана двухэтапная процедура верификации, позволяющая верифицировать как исходное секвенциальное описание, так и получаемый из него результат - систему булевых формул.

Разработано программное обеспечение, позволяющее конечному пользователю решать на ПЭВМ задачу преобразования словесных описаний алгоритмов управления технологическими процессами в систему булевых формул, т.е. получать “смысл” или “истину” в виде булевых формул из “текста”.

Результаты исследования упрощают интерактивную обработку исходной информации для существующих логических процессоров, а также являются средством эффективной поддержки при комплектации пакетов прикладных программ из наличного набора программных средств на разных уровнях моделирования.

Таким образом решена задача порождения системы булевых формул непосредственно из текста технического задания с помощью ПЭВМ. Кроме этого, предлагаемый подход показывает переспективность перехода от естественно - языкового метода представления технической информации к аналитическому, что дает возможность не только получать конкретные результаты, но и проводить дальнейшие исследования в этом направлении.

Ключевые слова: система, булевы формулы, техническое задание, продукция, Пост, условные секвенции, перевод, естественный, промежуточный, искусственный язык, утверждения, верификация.

ABSTRACT

Mr. Gutsa O. M. Interactive model of technical duties translation into system of Bull formulas.- Manuscript.

The Dissertation thesis on the Scientific degree of Ph.D. in technical sciences in specialty 01.05.02.- Mathematical modeling and computer methods. - Kharkiv National University of Radio-electronics, Kharkiv, 2002.

The author solved the problem of direct emergence of Bull formulas system from the text of technical task with the aid of personal computer. Used the model of “text-sense”. Proved 10 assertions which served as a program to give the possibility to the ultimate personal computer user to receive the result for its technological process control. This research had been oriented to these ultimate personal computer users because it gives the possibilities to solve the practical tasks proceeding from the wordy described model of control of technological processes including with the aid of program elaborated by the author. He had tried to verify the conformity of this research to the require of conceptual and technological approach to the creation of the new information technologies. The author hopes this work will be considered as an attempt to create the system based on the knowledge and not on the old principle “just let it be”.

Key words: system, Bull formulas, technical task, production, Post, conditional sequience, translation, natural, intermediate, artificial language, assertion, verification.

Размещено на Allbest.ru