Логіки, орієнтовані на специфікації програм
Розглянуті композиційно-номінативні логіки, орієнтовані на специфікації програм. Такі логіки будуються в семантико- синтаксичному стилі на основі композиційно-номінативного підходу. Пропонується спектр композиційно-номінативних логік різних рівнів абстрактності та загальності. Для логік еквітонних...
Gespeichert in:
| Datum: | 2006 |
|---|---|
| Hauptverfasser: | , , |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
Інститут програмних систем НАН України
2006
|
| Schlagworte: | |
| Online Zugang: | http://dspace.nbuv.gov.ua/handle/123456789/1514 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Логіки, орієнтовані на специфікації програм / М.С. Нікітченко, С.С. Шкільняк, Л.Л. Омельчук // Проблеми програмування. — 2006. — N 2-3. — С. 17-24. — Бібліогр.: 28 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-1514 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-15142008-08-22T12:00:20Z Логіки, орієнтовані на специфікації програм Нікітченко, М.С. Шкільняк, С.С. Омельчук, Л.Л. Теоретичні та методологічні основи програмування Розглянуті композиційно-номінативні логіки, орієнтовані на специфікації програм. Такі логіки будуються в семантико- синтаксичному стилі на основі композиційно-номінативного підходу. Пропонується спектр композиційно-номінативних логік різних рівнів абстрактності та загальності. Для логік еквітонних квазіарних предикатів на основі секвенційних числень доведені тео- реми про визначність. На базі аксіоматичної системи специфікацій програм над метаномінативними даними побудовано прототип системи автоматизації доведення теорем теорії МНД. Composition nominative logics oriented on program specification are considered. Such logics based on composition nominative approach are constructed in a semantic-syntactic style. The spectrum of logics of various abstraction and generality levels is developed. The definability theorems are proved based on the sequent calculi for logics of equitone quasiare predicates. The prototype of automatic theorem prover is constructed for the axiomatic system of program specification over metanominative data. 2006 Article Логіки, орієнтовані на специфікації програм / М.С. Нікітченко, С.С. Шкільняк, Л.Л. Омельчук // Проблеми програмування. — 2006. — N 2-3. — С. 17-24. — Бібліогр.: 28 назв. — укр. 1727-4907 http://dspace.nbuv.gov.ua/handle/123456789/1514 510.6, 681.3.06 uk Інститут програмних систем НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Ukrainian |
| topic |
Теоретичні та методологічні основи програмування Теоретичні та методологічні основи програмування |
| spellingShingle |
Теоретичні та методологічні основи програмування Теоретичні та методологічні основи програмування Нікітченко, М.С. Шкільняк, С.С. Омельчук, Л.Л. Логіки, орієнтовані на специфікації програм |
| description |
Розглянуті композиційно-номінативні логіки, орієнтовані на специфікації програм. Такі логіки будуються в семантико-
синтаксичному стилі на основі композиційно-номінативного підходу. Пропонується спектр композиційно-номінативних логік
різних рівнів абстрактності та загальності. Для логік еквітонних квазіарних предикатів на основі секвенційних числень доведені тео-
реми про визначність. На базі аксіоматичної системи специфікацій програм над метаномінативними даними побудовано прототип
системи автоматизації доведення теорем теорії МНД. |
| format |
Article |
| author |
Нікітченко, М.С. Шкільняк, С.С. Омельчук, Л.Л. |
| author_facet |
Нікітченко, М.С. Шкільняк, С.С. Омельчук, Л.Л. |
| author_sort |
Нікітченко, М.С. |
| title |
Логіки, орієнтовані на специфікації програм |
| title_short |
Логіки, орієнтовані на специфікації програм |
| title_full |
Логіки, орієнтовані на специфікації програм |
| title_fullStr |
Логіки, орієнтовані на специфікації програм |
| title_full_unstemmed |
Логіки, орієнтовані на специфікації програм |
| title_sort |
логіки, орієнтовані на специфікації програм |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2006 |
| topic_facet |
Теоретичні та методологічні основи програмування |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/1514 |
| citation_txt |
Логіки, орієнтовані на специфікації програм / М.С. Нікітченко, С.С. Шкільняк, Л.Л. Омельчук // Проблеми програмування. — 2006. — N 2-3. — С. 17-24. — Бібліогр.: 28 назв. — укр. |
| work_keys_str_mv |
AT níkítčenkoms logíkioríêntovanínaspecifíkacííprogram AT škílʹnâkss logíkioríêntovanínaspecifíkacííprogram AT omelʹčukll logíkioríêntovanínaspecifíkacííprogram |
| first_indexed |
2025-07-02T04:56:14Z |
| last_indexed |
2025-07-02T04:56:14Z |
| _version_ |
1836509744732307456 |
| fulltext |
Теоретичні і методологічні основи програмування
© И.В. Редько, 2006
ISSN 1727-4907. Проблеми програмування. 2006. № 2-3. Спеціальний випуск 17
УДК 510.6, 681.3.06
ЛОГІКИ, ОРІЄНТОВАНІ НА СПЕЦИФІКАЦІЇ ПРОГРАМ
М.С. Нікітченко, С.С. Шкільняк, Л.Л. Омельчук
Кафедра теорії та технології програмування Київського національного університету ім. Тараса Шевченка
м. Київ, тел. (044) 259 0519
е-mail: nikitchenko@unicyb.kiev.ua, sssh@unicyb.kiev.ua, ttp@unicyb.kiev.ua.
Розглянуті композиційно-номінативні логіки, орієнтовані на специфікації програм. Такі логіки будуються в семантико-
синтаксичному стилі на основі композиційно-номінативного підходу. Пропонується спектр композиційно-номінативних логік
різних рівнів абстрактності та загальності. Для логік еквітонних квазіарних предикатів на основі секвенційних числень доведені тео-
реми про визначність. На базі аксіоматичної системи специфікацій програм над метаномінативними даними побудовано прототип
системи автоматизації доведення теорем теорії МНД.
Composition nominative logics oriented on program specification are considered. Such logics based on composition nominative approach
are constructed in a semantic-syntactic style. The spectrum of logics of various abstraction and generality levels is developed. The defin-
ability theorems are proved based on the sequent calculi for logics of equitone quasiare predicates. The prototype of automatic theorem
prover is constructed for the axiomatic system of program specification over metanominative data.
Вступ
Розвиток інформаційних технологій та програмування веде до розширення сфери застосування матема-
тичної логіки. Стосовно загальносвітоглядного аспекту поняття і методів математичної логіки дають обґрунту-
вання правильності тих чи інших способів отримання істинного знання. До прагматичного аспекту апарат ма-
тематичної логіки належить до основних засобів моделювання різноманітних предметних областей, він є осно-
вою, ядром сучасних інформаційних та програмних систем, потужним засобом специфікацій програм. Пробле-
ма побудови адекватних логічних формалізмів специфікацій програм в наш час набуває особливої актуальності.
Для вирішення такої проблеми дуже плідним нам видається композиційно-номінативний підхід [1]. Основна
мета підходу полягає в побудові формальних моделей програм на різних рівнях абстрактності та загальності.
Він дає змогу побудувати широкий спектр логічних формалізмів на єдиній з програмуванням концептуальній
основі.
Згідно композиційно-номінативного підходу логіки будуємо в семантико-синтаксичному стилі. Це озна-
чає, що спочатку фіксуємо рівень абстракції розгляду предметних областей. Такі рівні відрізняються тракту-
ванням рівня абстракції множини даних. Потім будуємо відповідні розглянутому рівню абстракції математичні
моделі предметних областей, які задають семантичні аспекти логік. Семантичними моделями композиційно-
номінативних логік є предикатні композиційно-номінативні системи (ПКНС) [2]. Основою ПКНС є компози-
ційні алгебри предикатів. Нарешті, будуємо формально-аксіоматичні логічні числення, що задають синтаксичні
аспекти логік. Відомі дві основні різновидності таких систем – Гільбертівські (формальні системи) та Генценів-
ські (секвенційні системи).
1. Спектр композиційно-номінативних логік
Побудову композиційно-номінативних логік починаємо з гранично абстрактних рівнів, поступово їх кон-
кретизуючи.
На пропозиційному рівні дані трактуються гранично абстрактно, як "чорні" скриньки. На цьому рівні
предикати мають вигляд A→ { T, F}, де A – множина абстрактних даних.
Базовими композиціями фінітарних пропозиційних логік є Клінієві композиції диз'юнкції ∨∨∨∨ та запере-
чення ¬¬¬¬.
Базовими композиціями інфінітарних пропозиційних логік [3] є інфінітарні множинні диз'юнкція ∨∨∨∨К,
кон'юнкція &&&&К та композиція заперечення ¬¬¬¬К .
Сингулярний рівень може трактуватися як гранична конкретизація пропозиційного. У цьому випадку да-
ні трактуються гранично конкретно, як "білі" скриньки. На сингулярному рівні фіксується єдиний клас даних,
що пояснює його нaзву.
Теоретичні і методологічні основи програмування
18
Композиціями сингулярного рівня є максимально конкретні аплікативні композиції. Практично кожний
логічний засіб може трактуватися як аплікативна композиція. Для дослідження сингулярних логік збудована [3]
спеціальна інфінітарна алгебра сингулярних композицій Кліні.
Подальший розвиток приводить до класів логік, для яких рівень розгляду даних є синтезом двох перших
рівнів. На цьому рівні дані розглядаються як "сірі" скриньки, побудовані з "білих" і "чорних". Такі дані назива-
ються номінативними. Вони будуються індуктивно із множини предметних імен та множини предметних зна-
чень. Відповідні логіки будемо відносити до номінативного рівня, який дуже багатий і розпадається на низку
підрівнів.
На рівні іменних множин дані – це однозначні відображення типу V→A із множини предметних імен V у
множину предметних значень A. Такі 1-рівневі однозначні номінативні дані називають іменними множинами
(ІМ). Множину всіх V-ІМ над A позначаємо VA.
Функції, задані на іменних множинах, називають квазіарними.
Для логіки природно розглядати квазіарні функції двох типів.
Відображення вигляду VA→{ T, F} назвемо V-квазіарними предикатами на A.
Відображення вигляду VA→А назвемо V-квазіарними функціями на A.
Множини V-квазіарних предикатів та функцій на A позначаємо відповідно PrА та FnА.
V-квазіарний предикат Р (частково) істинний, якщо для довільних d∈VA із умови Р(d)↓ випливає
Р(d)=Т.
Найабстрактнішими серед логік номінативного рівня є реномінативні логіки. Починаючи з реномінативно-
го рівня можна перейменовувати компоненти даних. Це дає змогу ввести композицію реномінації (переймену-
вання).
Фінітарна реномінативна логіка запропонована в [4]. Базовими композиціями фінітарних реномінативних
логік є ∨∨∨∨, ¬¬¬¬ та реномінація R v
x . Для таких логік побудовані числення Гільбертівського типу та Генценівсько-
го типу, доведені коректність і повнота таких числень.
Інфінітарна реномінативна логіка екваційного типу запропонована в [5]. Базовими композиціями інфінітар-
них реномінативних логік є ∨∨∨∨К, &&&&К, ¬¬¬¬К та інфінітарна реномінація R
ρρρρ. Побудоване екваційне числення інфіні-
тарної реномінативної логіки, доведені його коректність і повнота.
На кванторному рівні можна застосовувати квазіарні предикати до всіх предметних значень. Це дозво-
ляє ввести композиції квантифікації ∃∃∃∃x та ∀∀∀∀x.
Фінітарні логіки кванторного рівня досліджувались, зокрема, в [6–8]. Базовими композиціями таких логік
є ∨∨∨∨, ¬¬¬¬, R v
x , ∃∃∃∃x.
Інфінітарна логіка кванторного рівня запропонована в [9]. Базовими композиціями інфінітарних кванто-
рних логік є ∨∨∨∨К, & К, ¬¬¬¬К, R
ρρρρ, ∃∃∃∃x.
На кванторно-екваційному рівні з’являються можливості ототожнення і розрізнення значень за допо-
могою спеціальних предикатів рівності =ху .
Фінітарні логіки кванторно-екваційного рівня досліджені в [10]. Базовими композиціями таких логік є ∨∨∨∨,
¬¬¬¬, R v
x , ∃∃∃∃x.
На функціональному рівні маємо розширені можливості формування нових аргументів для функцій та
предикатів. Це дає змогу ввести композицію суперпозиції S x . Базовими композиціями функціонального рівня
є ∨∨∨∨, ¬¬¬¬, R v
x , ∃∃∃∃x, Sx .
Для роботи з окремими компонентами даних в множині FnА природно виділити множину спеціальних
функцій деномінації (розіменування) Nf А ={ 'v| v∈V}. При введенні функцій розіменування 'x композиції ре-
номінації можна промоделювати за допомогою суперпозиції, тому базовими композиціями функціонального
рівня вважаємо ∨∨∨∨, ¬¬¬¬, ∃∃∃∃x, Sx .
На функціонально-екваційному рівні можна ототожнювати і розрізняти предметні значення. Це дає
змогу додатково ввести спеціальну композицію рівності =. Базовими композиціями функціонально-екваційного
рівня є ∨∨∨∨, ¬¬¬¬, ∃∃∃∃x, Sx , =.
Логіки функціонального та функціонально-екваційного рівня досліджувались, зокрема, в [11–13].
На наступному рівні абстракції елементи множини А можна розглядати як ієрархічні номінативні дані.
Відповідні логіки названі логіками номінативних даних (ЛНД). Такі логіки досліджені в [14].
ЛНД будуються у стилі теорії допустимих множин на основі властивостей відношення номінативної на-
лежності. Доведена коректність (несуперечливість) аксіоматичної теорії номінативних даних.
На основі ЛНД визначається клас багатозначних натурально (абстрактно) обчислюваних функцій над но-
мінативними даними. Такий клас можна подати [14] за допомогою ΣΣΣΣ-предикатів ЛНД.
Наведемо ієрархію композиційно-номінативних логік часткових предикатів за рівнем абстракції розгля-
ду.
Теоретичні і методологічні основи програмування
19
Пропозиційний рівень Сингулярний рівень
Номінативний рівень
Рівень іменних множин Ієрархічно-номінативний рівень
Реномінативний рівень
Кванторний рівень
Кванторно-екваційний рівень
Функціональний рівень
Функціонально-екваційний рівень
2. Логіки квазіарних предикатів
Семантичною основою логік квазіарних предикатів є композиційні алгебри квазіарних предикатів
(РrA, C). Для логік функціонального та функціонально-екваційного рівнів такою основою є композиційні алгеб-
ри квазіарних функцій і предикатів (РrA∪FnА, C). При фіксуванні множини базових композицій композиційна
алгебра визначається алгебраїчною системою (АС) А = (А, РrA). Для функціонального та функціонально-
екваційного рівнів така АС набуває вигляду А = (А, РrA∪FnА).
Побудова композиційної алгебри дає змогу задати [13] мову логіки відповідного рівня. Формули мови
логіки є термами такої предикатної алгебри.
Для формул мови логіки природним чином вводимо [13, 15] поняття:
– істинності формули Φ на моделі (АС) А: А|=Φ;
– всюди істинності формули Φ: |=Φ;
– логічного наслідку |=, слабкого логічного наслідку ||=;
– логічної еквівалентності ∼ ;
– логічного наслідку для множин формул |= .
Клас квазіарних предикатів дуже потужний, для логік квазіарних предикатів не діють деякі важливі зако-
ни класичної логіки. Наприклад, в загальному випадку квазіарних предикатів маємо |=Φ ⇒ |=∀хΦ, але не зав-
жди |=∀хΦ. Таким чином, для збереження основних властивостей класичної логіки клас квазіарних предикатів
варто обмежити.
Природне обмеження задається властивістю еквітонності, яка означає, що значення відображення не змі-
нюється при розширенні, поповненні даних.
Предикат Р еквітонний (ЕП), якщо для довільних d, d'∈VA із d'⊇d та Р(d)↓ випливає Р(d')↓=Р(d).
Найближчими до класичної логіки є логіки повнототальних еквітонних предикатів (ПЕП). Повнототаль-
ність означає визначеність предикату на максимальних даних – V-повних ІМ.
V-повна ІМ – це тотальна однозначна функція із V в A.
Множину всіх V-повних ІМ над A позначимо AV.
Предикат P повнототальний, якщо P(d)↓ для всіх d∈AV.
Логіки повнототальних еквітонних предикатів названі [8] неокласичними (НКЛ), оскільки вони зберіга-
ють основні закони та правила виведення класичної логіки при істотному розширенні класу моделей.
Логіки еквітонних предикатів зберігають основні закони класичної логіки, але для них вже не діють деякі
правила виведення (modus ponens), порушуються деякі властивості класичної логіки.
Наприклад, для конкретних семантичних моделей можливо A |=P, A |=P→Q, але A |≠Q.
Можливо також A |=P↔Q, A |=Q↔S, але A |≠P↔S.
Крім того, для логіки ЕП не завжди із Φ|=Ψ випливає Φ||=Ψ.
Клас моделей логіки ЕП істотно ширший за клас моделей логіки ПЕП.
Семантичні властивості логіки ЕП фактично відтворюють [13] властивості композицій. Зокрема, власти-
вості, які не використовують реномінації та суперпозиції, цілком аналогічні відповідним властивостям класич-
ної логіки предикатів.
Для логіки ЕП справджуються [13] теореми семантичної еквiвалентостi та рівності, а стосовно відношен-
ня логічного наслідку для множин формул – теорема про заміну еквівалентних [15].
Для формул класичної логіки істотними є тільки їх вільні предметні імена, від яких може залежати зна-
чення відповідних предикатів. Для логік ЕП важлива неістотність предметних імен. Тому для базових преди-
катів логіки ЕП будемо вказувати множину неістотних імен, від яких не залежить значення таких предикатів.
Можливість виконання еквівалентних перетворень довільних формул вимагає наявності нескінченної множини
Теоретичні і методологічні основи програмування
20
тотально неістотних імен, тобто імен, неiстотних для кожного р∈Ps. Таким чином, семантичною основою логі-
ки ЕП є композиційні алгебри еквітонних квазіарних предикатів з додатковою вимогою наявності нескінченної
множини тотально неістотних предметних імен.
Для формул логіки ЕП визначаються субнормальні (різнокванторні), нормальні, квазізамкнені формули.
Доводиться [13, 15], що для кожної формули можна збудувати еквівалентні їй різнокванторну та нормальну
формули.
Квазізамкнені формули є синтаксичними аналогами замкнених формул класичної логіки, але семантич-
ними аналогами їх вважати не можна. Квазізамкнені формули необов'язково інтерпретуються як константні
предикати, хоча для класичної логіки кожна замкнена формула на кожній АС завжди інтерпретується як тотож-
на істина або тотожна фальш. Справа в тому, що до складу формули логіки квазіарних предикатів можуть вхо-
дити предикатні символи, для яких множини істотних імен нескінченні.
Специфічну властивість квазізамкнених формул логіки ЕП описує наступна
Теорема 1. Нехай формула Φ квазізамкнена, її пропозиційна схема (пропозиційна формула, отримана із
Φ опусканням усіх символів, окрім предикатних символів та символів пропозиційних зв'язок) не тавтологія і не
суперечність, причому не містить спеціальних предикатних символів із явно виділеними істотними іменами
(наприклад, =ху). Тоді існують АС A = (A, I) та d1, d1∈VA такі, що ΦА(d1) = T та ΦА(d2) = F.
Можливість для формули бути залежною від нескінченної множини предметних імен є визначальною
властивістю логіки квазіарних предикатів, зокрема логіки ЕП, що істотно відрізняє її від класичної логіки.
Для логік повнототальних ЕП (неокласичних логік) будуються аксіоматичні системи Гільбертівського ти-
пу, на їх основі доводяться [7, 12] теореми коректності (несуперечливості) та повноти. Більше того, можна го-
ворити [8] про ізоморфне вкладення класичної логіки в неокласичну. Це випливає з того, що всі аксіоми класи-
чної логіки виводяться в неокласичній логіці, правила виведення класичної логіки моделюються в неокласичній
логіці. Звідси отримуємо моделювання виведень формул класичної логіки в неокласичній.
Проте універсального моделювання класу формул неокласичної логіки в класі формул класичної логіки
не існує. Причина полягає в тому, що кількість істотних змінних для формул неокласичної логіки може бути
нескінченною. Але ми можемо зробити обмежене моделювання, тому що, як зазначено вище, кожну формулу
неокласичної логіки можна звести до еквівалентної їй псевдокласичної нормальної форми, використовуючи
додаткові тотально неістотні предметні імена.
Відмова від modus ponens для загального випадку логік ЕП веде до необхідності проводити дослідження
синтаксичних властивостей таких логік на базі не Гільбертівських, а Генценівських систем – секвенційних числень. Семан-
тичною основою побудови таких числень є властивості відношення логічного наслідку для множин формул.
Такі числення збудовані [15–18] для логік ЕП відповідного рівня.
Для секвенційних числень доведені теореми коректності та повноти.
Теорема 2 (теорема коректності). Нехай секвенція |−|−|−|− ΓΓΓΓ−| −| −| −| ∆∆∆∆ вивідна. Тоді ΓΓΓΓ |= |= |= |= ∆∆∆∆.
Теорема 3 (теорема повноти). Нехай ΓΓΓΓ |= |= |= |= ∆∆∆∆. Тоді секвенція |−|−|−|− ΓΓΓΓ−| −| −| −| ∆∆∆∆ вивідна.
Природним узагальненням еквітонних предикатів є [19] локально-еквітонні предикати (ЛЕП). Для ло-
кально-еквітонних предикатів вимагається збереження значення при розширенні даних лише на скінченну кіль-
кість іменованих компонент.
Предикат Р локально-еквітонний, якщо для довільних d, d'∈VA із того, що Р(d)↓, d' ⊃d та d' \d скін-
ченна, випливає Р(d')↓=Р(d).
Клас ЛЕП є розширенням класу ЕП. Справді, предикат, істинний на всіх скінченних ІМ та хибний на всіх
нескінченних ІМ, є нееквітонним ЛЕП.
Семантичні властивості ЛЕП аналогічні властивостям ЕП. Клас моделей логіки ЛЕП є розширенням кла-
су моделей логіки еквітонних предикатів.
Логіки, орієнтовані на такі особливості предметних областей, як невизначеність, неповнота наявної інфор-
мації, базуються на класах предикатів, визначених на даних з неповною інформацією. Такими є [20] еквісумісні
предикати (ЕСП) та локально-еквісумісні предикати (ЛЕСП).
Еквісумісність предиката P означає, що при можливості розширення різних даних (сумісність даних) до
одного більшого даного, значення P на таких даних повинні співпадати. При локально-еквісумісності вимагаємо
збереження значень лише для розширень скінченною інформацією.
Еквісумісні та локально-еквісумісні предикати є узагальненнями еквiтонних та локально-еквітонних пре-
дикатів. Відомі [20, 21] приклади нееквітонних, але еквісумісних предикатів та приклади локально-
еквісумісних предикатів, які не є локально-еквітонними та не є еквісумісними.
Семантичні властивості логік ЕСП та ЛЕСП аналогічні відповідним властивостям логік ЕП та ЛЕП. Кла-
си семантичних моделей логік еквісумісних та локально-еквісумісних предикатів ще ширші, хоча ці логіки збе-
рігають основні закони класичної логіки.
Для логік ЛЕП, ЕСП та ЛЕСП збудовані [19, 20] числення секвенційного типу, для таких числень дове-
дені теореми коректності та повноти.
Із теореми повноти випливає [15] низка важливих властивостей логік ЕП, ЛЕП, ЕСП та ЛЕСП, зокрема
принцип компактності, теорема про існування моделі. На цій основі розглядаються питання семантичної та
синтаксичної несуперечливості, взаємної суперечливості та взаємної несуперечливості множин формул.
Теоретичні і методологічні основи програмування
21
Зауважимо, що секвенційні числення логік ЛЕП, ЕСП та ЛЕСП ідентичні секвенційним численням логік
ЕП. Це засвідчує той факт, що синтаксичні властивості логік ЛЕП, ЕСП та ЛЕСП аналогічні синтасичним влас-
тивостям логік ЕП. У той же час при переході від логік ЕП до логік ЛЕП та логік ЕСП, від логік ЛЕП та логік
ЕСП до логік ЛЕСП ми отримуємо все ширші класи семантичних моделей.
Наведемо тепер ієрархію логік квазіарних предикатів за обмеженнями на клас предикатів.
Класичні логіки скінченно-арних тотальних предикатів
Логіки повнототальних еквітонних предикатів
Логіки еквітонних предикатів
Логіки локально-еквітонних предикатів
Логіки еквісумісних предикатів
Логіки локально-еквісумісних предикатів
Логіки квазіарних предикатів
3. Інтерполяційна теорема. Теореми про визначність
Одним з найважливіших результатів математичної логіки є інтерполяційна теорема [22, 23]). Вона справ-
джується також [24] для логіки ЕП.
Теорема 4 (інтерполяційна теорема). Нехай секвенція −|−|−|−|Ψ→Ξ має виведення. Тоді існує формула Φ си-
гнатури σ(Φ)⊆σ(Ψ)∩σ(Ξ) така, що секвенції −|−|−|−|Ψ→Φ та −|−|−|−|Φ→Ξ мають виведення.
Таку Φ називають інтерполяційною формулою або інтерполянтом.
При σ(Ψ)∩σ(Ξ) = ∅ твердження теореми може бути невірним (це відзначено, зокрема, в [22]). Напри-
клад, нехай Ψ та Ξ – це формули ¬p∨p та ¬q∨q, де p, q∈Ps. Тоді інтерполянтом Φ буде всюди істинна
формула, але при умові σ(Φ)⊆σ(Ψ)∩σ(Ξ) = ∅ такої формули Φ не існує, оскільки її просто немає з чого буду-
вати.
Як і у випадку класичної логіки [23], для логіки ЕП доводиться загальніша
Теорема 5. Нехай секвенція ΣΣΣΣ = ΣΣΣΣ1, ΣΣΣΣ2 має виведення δδδδ. Тоді існує формула Φ сигнатури
σ(Φ)⊆σ(ΣΣΣΣ1)∩σ(ΣΣΣΣ2) така, що за δδδδ можна збудувати виведення δδδδ1 для секвенції −|−|−|−|Φ, ΣΣΣΣ1 та виведення δδδδ2 для
секвенції |−|−|−|−Φ, ΣΣΣΣ2 .
Теорема доводиться індукцією за довжиною виведення.
Розглянемо співвідношення між двома різними уточненнями визначення одного поняття в термінах ін-
ших понять.
Одне уточнення – семантичне, або неявне. Його суть: поняття (предикатний символ) q неявно визнача-
ється через поняття p1,…, pn в теорії (множині формул) ΓΓΓΓ, якщо для кожних моделей істинності ΓΓΓΓ, узгоджених
у тому розумінні, що в них p1,…, pn інтерпретуються однаково, маємо однакові інтерпретації для q.
Друге уточнення – синтаксичне, або явне. Його суть: поняття q явно визначається в ΓΓΓΓ через поняття
p1,…, pn, якщо таке визначення є логічним наслідком ΓΓΓΓ.
Для класичної логіки еквівалентність явного та неявного визначень одного поняття в термінах інших по-
нять – це теорема Бета про визначність. Аналогічний результат справджується і для логіки квазіарних еквітон-
них предикатів.
Розглядаємо мову певної сигнатури, множини формул мови, семантичні моделі мови – неокласичні АС
відповідної сигнатури.
Будемо дотримуватись позначень роботи [15].
Нехай p ⊆Ps – деяка множина предикатних символів мови.
Моделлю істинності множини формул ΓΓΓΓ назвемо довільну АС A = (A, I ) таку, що для кожних d∈VA та
Φ∈ΓΓΓΓ маємо ΦА(d) ≅ T.
Модель A еквітонна (локально-еквітонна) якщо для кожного p∈Ps предикат pА еквітонний (локально-
еквітонний).
Моделі істинності A=(M, IA) та В=(M, IВ) множини формул ΓΓΓΓ p -тотожні, якщо для кожного p∈ p
маємо pA ≅ pВ .
Теоретичні і методологічні основи програмування
22
Предикатний символ q семантично визначний через предикатні символи { p1,…, pn}, де q∉{ p1,…, pn},
якщо для кожних {p1,…, pn}- тотожних еквітонних моделей істинності A=(M, IA) та В=(M, IВ) множини формул
ΓΓΓΓ маємо qA ≅ qВ .
Предикатний символ q синтаксично визначний через предикатні символи { p1,…, pn} в множині формул
ΓΓΓΓ, якщо існує формула Φ із σ(Φ) ={p1,…, pn} така, що ΓΓΓΓ |=|=|=|= q↔Φ.
Теорема 6. Нехай ПС q синтаксично визначний через {p1,…, pn} в множині формул ΓΓΓΓ. Тоді q семан-
тично визначний через {p1,…, pn}.
Нехай формула Φ із σ(Φ) ={p1,…, pn} така, що ΓΓΓΓ |=|=|=|= q↔Φ. Припустимо супротивне: q не є семантично
визначним через {p1,…, pn}. Тоді існують {p1,…, pn}- тотожні еквітонні моделі істинності A=(M, IA) та
В=(M, IВ) для ΓΓΓΓ та d∈VM такі, що qA(d) ≠ qВ(d).
Візьмемо для A та В АС повнототальних розширень A' та В' відповідно, візьмемо δ∈MV таке, що
δ⊇d. За еквітонністю тоді qA' (δ) = qA(d), qB' (δ) = qB(d), тому qA' (δ) ≠ qВ' (δ). Але A' та В' – моделі істинності
для ΓΓΓΓ, тому для всіх Ψ∈ΓΓΓΓ маємо ΨA'(δ) = T, ΨB'(δ) = T. Враховуючи ΓΓΓΓ |=|=|=|= q↔Φ, тоді (q↔Φ)A' (δ) = T та
(q↔Φ)В' (δ) = T, але згідно qA' (δ) ≠ qВ' (δ) маємо ΦA' (δ) ≠ ΦВ' (δ). Проте σ(Φ) ={p1,…, pn}, A' та В' –
{ p1,…, pn}- тотожні, тому ΦA' (δ) = ΦВ' (δ). Отримали суперечність ▄
Зауваження. Можливо ΓΓΓΓ |=|=|=|= q↔Φ, але для p -тотожних локально-еквітонних моделей істинності
A=(M, IA) та В=(M, IВ) для ΓΓΓΓ можливо qA ≠ qВ. Справді, візьмемо як Φ предикатний символ p, візьмемо
ΓΓΓΓ ={q↔p}. Задамо qA(d) = F для скінченних d та qA(d) = Т для нескінченних d, qB(d) = T для довільних d;
задамо pA(d)↑ та pB(d)↑ для скінченних d, pA(d) = pB(d) = Т для нескінченних d. Для скінченних d маємо
(q↔p)A(d)↑ та (q↔p)B(d)↑, для нескінченних d маємо (q↔p)A(d) = T та (q↔p)B(d) = T. Але q↔p |=|=|=|= q↔p,
тому A та В – моделі істинності для ΓΓΓΓ ={q↔p}. У той же час qA ≠ qВ.
Теорема 7. Нехай предикатний символ q семантично визначний через {p1,…, pn}. Тоді q синтаксично
визначний через {p1,…, pn} в множині формул ΓΓΓΓ.
Згідно умови для довільних {p1,…, pn}- тотожних еквітонних моделей істинності A=(M, IA) та В=(M, IВ)
множини формул ΓΓΓΓ маємо qA ≅ qВ . Покажемо, що існує формула Φ із σ(Φ) ={p1,…, pn} така, що ΓΓΓΓ |=|=|=|= q↔Φ.
Продублюємо як β' кожний ПС β∈Ps \{ p1,…, pn}. При цьому задаємо µ(β')=µ(β), IA(β')=IA(β),
IB(β')=IB(β). При заміні кожного β на β' кожна формула Ψ∈ΓΓΓΓ переходить у формулу Ψ', множина ΓΓΓΓ – у ΓΓΓΓ' .
При цьому ΨA = Ψ'A, ΨB = Ψ'B. Кожна модель істинності M=(M, IM) множини формул ΓΓΓΓ ізоморфно перетво-
рюється у модель істинності M'=(M, IM') множини формул ΓΓΓΓ' .
Позначимо I ∪ = IM ∪IM' . Тоді M∪∪∪∪ =(M, I∪) – модель істинності множини формул ΓΓΓΓ∪ΓΓΓΓ' . Маємо
I∪(q) = IM(q) = IM' (q') = I∪(q'). Звідси ΓΓΓΓ∪ΓΓΓΓ' |=|=|=|= q↔q'. Згідно теореми повноти секвенція |−|−|−|−ΓΓΓΓ∪ΓΓΓΓ'−|−|−|−| q↔q' вивідна,
вона має скінченне замкнене секвенційне дерево δδδδ. При побудові δδδδ використовуються лише формули деякої
скінченної cеквенції ΓΓΓΓ0∪ΓΓΓΓ'0
⊆ ΓΓΓΓ∪ΓΓΓΓ' . Отримуємо дерево δδδδ0 з коренем |−|−|−|−ΓΓΓΓ0∪ΓΓΓΓ'0 −|−|−|−| q↔q', всі вершини якого −
скінченні секвенції. Отже, скінченна секвеція |−|−|−|−ΓΓΓΓ0∪ΓΓΓΓ'0 −|−|−|−| q↔q' вивідна. Нехай ΓΓΓΓ0∪ΓΓΓΓ'0 = {A 1,…, Am, B1,…, Bk},
де ΓΓΓΓ0 = {A 1,…, Am}, ΓΓΓΓ'0\ΓΓΓΓ0 = {B 1,…, Bk}. Формули A1&…&A m та B1&…&B k позначимо A та B відповідно.
Тоді секвеція |−|−|−|−A&B −|−|−|−| q↔q' вивідна, звідки A&B |=|=|=|= q↔q'. Звідси |=A&B →(q↔q'), що рівносильно
|=(A& q→B→q')&(A& ¬q→B→¬q'), тому |=A& q→B→q' та |=A& ¬q→B→¬q'. Отже, секвенції −|−|−|−|A& q→B→q'
та −|−|−|−|A& ¬q→B→¬q' вивідні.
Згідно інтерполяційної теореми для вивідної секвенції −|−|−|−|A& q→B→q' існує формула Φ сигнатури
σ(Φ)⊆σ(A& q)∩σ(B→q') така, що −|−|−|−|A& q→Φ та −|−|−|−|Φ→B→q' вивідні. Але
σ(A& q)∩σ(B→q') = σ(A)∩σ(B) ⊆ σ(ΓΓΓΓ)∩σ(ΓΓΓΓ'), σ(ΓΓΓΓ)∩σ(ΓΓΓΓ') = { p1,…, pn}. Тому σ(Φ) ⊆ { p1,…, pn}.
Із вивідності −|−|−|−|A& q→Φ та −|−|−|−|Φ→B→q' випливає вивідність секвенцій −|−|−|−|A→q→Φ та −|−|−|−|B→Φ→q'. Звідси
вивідні секвенції |−|−|−|−A−|−|−|−|q→Φ та |−|−|−|−B−|−|−|−|Φ→q', отже, вивідні секвенції |−|−|−|−ΓΓΓΓ−|−|−|−| q→Φ та |−|−|−|−ΓΓΓΓ'−|−|−|−|Φ→q'. Продублюємо сек-
венційне дерево для |−|−|−|−ΓΓΓΓ'−|−|−|−|Φ→q', знімаючи '. Отримаємо виведення секвенції |−|−|−|−ΓΓΓΓ−|−|−|−|Φ→q. Із виведень секвенцій
|−|−|−|−ΓΓΓΓ−|−|−|−| q→Φ та |−|−|−|−ΓΓΓΓ−|−|−|−|Φ→q дістаємо виведення секвенції |−|−|−|−ΓΓΓΓ−| −| −| −| q↔Φ. Звідси ΓΓΓΓ |=|=|=|= q↔Φ ▄
Зауважимо, що при застосуванні інтерполяційної теореми до вивідної секвенції −|−|−|−|A& ¬q→B→¬q отри-
муємо формулу Ξ таку, що σ(Ξ) ⊆{ p1,…, pn} та секвенція |−|−|−|−ΓΓΓΓ−| −| −| −| ¬q↔Ξ вивідна. Звідси ΓΓΓΓ |=|=|=|= ¬q↔Ξ, тобто
Ξ∼¬Φ.
4. Автоматизована система доведення теорем теорії метаномінативних даних
З метою побудови адекватних формалізмів специфікацій недетермінованих програм в [25] запропонована
аксіоматична система специфікацій програм над метаномінативними даними (МНД). Така система є достатньо
багатою, вона дозволяє доводити низку важливих властивостей часткових багатозначних функцій, а також про-
водити подальшу конкретизацію специфікацій у мовах програмування більш низького рівня. Базуючись на ак-
сіоматичній системі специфікацій програм над МНД, секвенційних численнях фінітарних КНЛ та запропонова-
ному в [26] секвенційному численні сннгулярних КНЛ, ми пропонуємо прототип системи автоматизації дове-
дення теорем теорії метаномінативних даних.
Система Автоматизації Доведення теорем теорії Метаномінативних Даних (САДМД) будується на основі
відомої Системи Автоматизації Дедукції (САД) [27]. Структура САДМД аналогічна структурі САД.
Теоретичні і методологічні основи програмування
23
САДМД може орієнтуватися на сингулярні КНЛ або на фінітарні КНЛ 1-го порядку. САДМД забезпечує
введення тексту у вигляді секвенції відповідної мови та здійснює пошук виведення такої секвенції.
Ядром САДМД є програма alice. Вона обробляє вхідний текст, використовуючи вбудований reasoner.
Посередником між alice та зовнішніми пруверами є програма haigha. Ці програми не призначені для безпосере-
днього використання. Інтерфейс для їх функціонування забезпечується сценарієм sad-moses. Аксіоми теорії
метаномінативних даних [25] описані окремим файлом.
САДМД функціонує наступним чином. Спочатку вона переводить вхідний текст, записаний у вигляді
секвенції мови КНЛ першого порядку, в його внутрішнє представлення. В переведеному тексті система обирає
множину цілей (твердження, які доводяться) та для кожної цілі визначає набір її логічних попередників (твер-
дження, які потрібно використовувати в доведенні). Нарешті, за допомогою відповідного прувера система про-
бує виводити кожну ціль із її попередників.
Програма alice містить такі основні модулі: [FOL], [TPTP], [Reason] та [Moses]. Наведемо їх короткий
опис.
Модуль [FOL]. Виконує розбір вхідних текстів. Він перетворює вхідний текст, записаний у вигляді сек-
венції мови КНЛ, у відповідне внутрішнє представлення.
Модуль [TPTP]. Об’єднує САДМД з відомою TPTP-бібліотекою, яка містить кілька тисяч логічних про-
блем для автоматизованих систем доведення.
Модуль [Reason]. Цей модуль керує верифікацією. Він формулює задачі верифікації та намагається їх
розв'язати, використовуючи власні еврістичні засоби, а також прувер САДМД та зовнішні прувери. Зокрема,
[Reason] розбиває складну ціль на множину більш простих.
Модуль [Moses]. Це прувер САДМД, він призначений для пошуку виведення на основі відповідного сек-
венційного числення. Moses може орієнтуватися на числення сингулярних КНЛ або на числення фінітарних
КНЛ 1-го порядку. Прувер переглядає область пошуку, використовуючи обмежений пошук в глибину. Для під-
вищення ефективності пошуку виведення [Moses] використовує спеціальні обмеження і техніку згортання [28].
САДМД протестована на прикладах. Це засвідчує, що пропонована система дозволяє доводити низку
властивостей програм.
Висновки
Розглянуті композиційно-номінативні логіки, які орієнтовані на специфікації програм. Такі логіки буду-
ються в семантико-синтаксичному стилі на основі композиційно-номінативного підходу. Пропонується спектр
композиційно-номінативні логік різних рівнів абстрактності та загальності. Для логік еквітонних квазіарних пре-
дикатів розглядаються інтерполяційна теорема і теореми про визначність, вони доводяться на основі секвенційних
числень. На базі аксіоматичної системи специфікацій програм над метаномінативними даними побудована сис-
тема автоматизації доведення теорем теорії МНД. Таким чином, композиційно-номінативний підхід може ефек-
тивно використовуватися для дослідження та побудови систем специфікацій програм над даними складної
структури.
1. Никитченко Н.С. Композиционно–номинативный подход к уточнению понятия программы // Пробл. программирования. – 1999. – №1.
– С. 16–31.
2. Никитченко Н.С. Предикатные композиционно–номинативные системы // Там же. – №2. – С. 3–19.
3. Никитченко Н.С. Пропозициональные композиции частичных предикатов // Кибернетика и системный анализ. – 2000. – № 2. – C. 3-19.
4. Шкільняк С.С. Безкванторні неокласичні логіки // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2001. – Вип. 4. – С. 323–331.
5. Нікітченко М.С. Інфінітарні реномінативні логіки часткових предикатів // Там же. – 2002. – Вип. 3. – C. 229–238
6. Нікітченко М.С., Шкільняк С.С. Композиційно-номінативні логіки еквітонних предикатів // Там же. – 2000. – Вип. 2. – С. 300–314.
7. Нікітченко М.С., Шкільняк С.С. Чисті композиційно-номінативні числення // Там же. – Вип. 3. – С. 290–303.
8. Никитченко Н.С., Шкильняк С.С. Неоклассические логики предикатов // Пробл. программирования. – 2000. – № 3–4. – C. 3–17.
9. Никитченко Н.С. Аппликативные композиции частичных предикатов // Кибернетика и системный анализ. – 2001. – № 2. – C. 14–33.
10. Шкільняк С.С. Неокласичні кванторні логіки з рівністю // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2003. – Вип.1. – С. 222–225.
11. Нікітченко М.С., Шкільняк С.С. Композиційно-номінативні логіки першого порядку // Там же. – 2001. – Вип.1. – С. 260–274.
12. Нікітченко М.С., Шкільняк С.С. Композиційно-номінативні числення першого порядку // Там же. – Вип. 2. – С. 302–313.
13. Нікітченко М.С., Шкільняк С.С. Математична логіка. К.: Київ. ун-т. – 2003. – 120 с.
14. Нікітченко М.С., Шкільняк С.С. Композиційні логіки номінативних даних // Пробл. программирования. – 2003. – № 3. – C. 29–40.
15. Нікітченко М.С., Шкільняк С.С. Математична логіка. Додаткові розділи. – К.: Київ. ун-т. – 2004. – 77 с.
16. Шкільняк С.С. Неокласичні секвенційні числення // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2002. – Вип.4. – С. 261–274.
17. Шкільняк С.С. Функціонально-екваційні неокласичні логіки: числення секвенційного типу // Там же. – 2003. – Вип. 4. – C. 302–309.
18. Шкільняк С.С. Фінітарні логіки квазіарних предикатів // Вісн. Київ. ун-ту. Сер.: кібернетика. – 2005. – Вип. 6. – С. 47–55.
19. Нікітченко М.С., Шкільняк С.С. Логіки локально-еквітонних предикатів: семантичні властивості та секвенційні числення // Пробл.
программирования. – 2003. – № 2. – C. 28–41.
20. Нікітченко М.С., Шкільняк С.С. Композиційно-номінативні логіки предикатів над даними з неповною інформацією // Там же. – 2004. –
№ 2–3. – C. 74–80.
21. Нікітченко М.С., Шкільняк С.С. Ієрархія композиційно-номінативних логік // Там же. – № 4. – С. 5 –14
22. Клини С. Математическая логика. – М.: Наука, 1973. – 480 с.
23. Непейвода Н.Н. Прикладная логика. – Новосибирск: НГУ, 2000. – 521 с.
24. Шкільняк С.С. Властивості неокласичних секвенційних числень // Вісн. Київ. ун-ту. Сер.: фіз.-мат. науки. – 2004. – Вип.1. – С. 286 –293.
25. Никитченко Н.С., Омельчук Л.Л., Шкильняк С.С., Янченко О.И. Аксиоматические системы спецификаций программ над номинативными
данными // Пробл. программирования. – 2000. – № 1-2. – С. 259–272.
Теоретичні і методологічні основи програмування
24
26. Омельчук Л.Л. Секвенційне числення для композиційно-номінативних логік часткових предикатів // Вісн. Київ. ун-ту. Сер.: фіз.-мат.
науки. – 2003. – Вип.4. – С. 270 –278.
27. Lyaletski A., Verchinine K., Degtyarev A., Paskevich A. System for Automated Deduction (SAD): Linguistic and deductive peculiarities // Intelli-
gent Information Systems 2002 (Proc. IIS’2002 Symp., Sopot, Poland) / Eds. M.A. Klopotek, S.T. Wierzchon, M. Michalewicz). – Physica-
Verlag, 2002. – P. 413–422.
28. Letz R., Stenz G. Model elimination and connection tableau procedures // Handbook for Automated Reasoning. Vol. II Eds.
A. Robinson, A. Voronkov. – Elsevier Science, 2001. – P. 2017–2116.
|