Symbolic models for single-conclusion proof logics

Автор: Krupski Vladimir N.
Сборник: Computer Science – Theory and Applications, 5th International Computer Science Symposium in Russia, CSR 2010, Kazan, Russia, June 16-20, 2010. Proceedings
Серия: Lecture Notes in Computer Science
Том: 6072
Год издания: 2010
Издательство: SPRINGER-VERLAG BERLIN
Местоположение издательства: HEIDELBERGER PLATZ 3, BERLIN, GERMANY,D-14197
Первая страница: 276
Последняя страница: 287
DOI: 10.1007/978-3-642-13182-0_26
Аннотация: Symbolic semantics for logics of proofs based on Mkrtychev models covers the the case of multi-conclusion proof logics. We propose symbolic models for single-conclusion proof logics (FLP and its extensions). The corresponding soundness and completeness theorems are proven. The developed symbolic model technique is used to establish the consistency of contexts required for proof internalization. In particular, we construct an extension of FLP that enjoys the strong proof internalization property with empty context.
Добавил в систему: Крупский Владимир Николаевич

	ИСТИНА	Войти в систему Регистрация
	ИСТИНА ЦЭМИ РАН
	Главная Поиск Статистика О проекте Помощь

ИСТИНА