|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
Operational Logic of Proofs with Functionality Condition on Proof Predicateстатья
- Автор: Krupski Vladimir
- Сборник: Logical Foundations of Computer Science, 4th International Symposium, LFCS'97, Yaroslavl, Russia, July 6-12, 1997, Proceedings
- Редактор: Адян Сергей Иванович
- Серия: Lecture Notes in Computer Science
- Том: 1234
- Год издания: 1997
- Место издания: Springer-Verlag Berlin
- Первая страница: 167
- Последняя страница: 177
- DOI: 10.1007/3-540-63045-7_18
- Аннотация: The extended operational (term-labeled modal) language is used to give the axiomatic description for functional proof predicate supplied with effective operations on proofs induced by modus ponens and necessitation rules. An additional operation is involved which restores a statement from its proof. The arithmetical completeness and decidability theorems are proved. The cut-elimination property for Gentzen style reformulation of corresponding logic is established. Partially supported by Grant INTAS-RFBR No. 95-0095 and by Grant RFBR No.96-01-01470.
- Добавил в систему: Золин Евгений Евгеньевич