|
ИСТИНА |
Войти в систему Регистрация |
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
Logic of proofs and labels with a complete set of operationsстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 18 июля 2013 г.
- Автор: Yavorskaya Tatiana
- Журнал: Journal of Logic and Computation
- Том: 16
- Номер: 5
- Год издания: 2006
- Издательство: Oxford University Press
- Местоположение издательства: United Kingdom
- Первая страница: 697
- Последняя страница: 710
- DOI: 10.1093/logcom/exl032
- Аннотация: We develop a framework in which operations on proofs can be specified and studied. Proofs are treated as structures built from atomic proofs and references by means of computable operations. Our approach extends the ideas of Logic of Proofs (Artemov, 1995, Bull. Symb. Logic, 7, 1–36) in which the proof predicate ‘t is a proof of F ’ is incorporated into the propositional language. We introduce an additional storage predicate ‘x is a label for F ’ (Yavorskaya, 2005, J. Logic Comput., 15, 517–537). In this article which is essentially a continuation of Yavorskaya's work, we study a natural example of a logic with operations on proofs and labels. This logic LPS* is decidable and complete with respect to its intended semantics. LPS* is capable to internalize its own proofs, and operations of LPS* suffice to realize all operations specified in the language with proofs and labels.
- Добавил в систему: Яворская Татьяна Леонидовна