Повнота секвенційних числень модальних логік немонотонних часткових предикатів

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

Ausführliche Beschreibung

Gespeichert in:
Bibliographische Detailangaben
Veröffentlicht in:Штучний інтелект
Datum:2016
Hauptverfasser: Шкільняк, О.С., Касьянюк, В.С., Малютенко, Л.М.
Format: Artikel
Sprache:Ukrainisch
Veröffentlicht: Інститут проблем штучного інтелекту МОН України та НАН України 2016
Schlagworte:
Online Zugang:https://nasplib.isofts.kiev.ua/handle/123456789/132074
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:Повнота секвенційних числень модальних логік немонотонних часткових предикатів / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Штучний інтелект. — 2016. — № 3. — С. 92-102. — Бібліогр.: 7 назв. — укр.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
Beschreibung
Zusammenfassung:Для чистих першопорядкових композиційно-номінативних модальних логік часткових немонотонних предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них вказано базові секвенційні форми та умови замкненості секвенцій, доведено їх коректність і повноту. Доведення теореми повноти опирається на теорему про існування контрмоделі для незамкненого шляху в секвенційному дереві, для її побудови використано метод систем модельних множин. In this paper we construct sequent calculi for pure first-order composition nominative modal logics of partial non-monotone predicates. We specify various variants of the introduced calculi, their basic sequent forms and sequent closure conditions. The proof of the completeness theorem is based on the theorem about existence of a counter-model for a non-closed path in a sequent tree; the counter-model is obtained using the Hintikka sets method.
ISSN:1561-5359