Correspondence analysis and automated proof-searching for first degree entailment

Petrukhin, Y.; Shangin, V.

Авторы: Petrukhin Yaroslav, Shangin Vasily
Журнал: European Journal of Mathematics
Том: 6
Номер: 4
Год издания: 2020
Издательство: Springer Nature
Местоположение издательства: Switzerland
Первая страница: 1452
Последняя страница: 1495
DOI: 10.1007/s40879-019-00344-5
Аннотация: In this paper, we present correspondence analysis for the well-known four-valued logic First Degree Entailment (FDE). Correspondence analysis is Kooi and Tamminga’s technique for finding adequate natural deduction systems for all the truth-functional unary and binary extensions of an arbitrary functionally incomplete many-valued logic. In particular, Kooi and Tamminga initially presented correspondence analysis for Asenjo–Priest’s three-valued the Logic of Paradox. Generally speaking, a tabular functionally incomplete many-valued logic is added with an arbitrary unary or binary connective ∘ following the truth-table definition of ∘. As a result, a tremendous amount of logics obtains a sound and complete natural deduction system in one go. In this paper, we generalize its application proposed by Kooi and Tamminga for the unary extensions of FDE and obtain correspondence analysis for the binary extensions of the logic in question. On the other hand, we use a proof-searching algorithm to have been successfully applied to classical and a variety of non-classical logics and present a finite, sound, and complete proof-searching algorithm for natural deduction systems for the binary extensions of FDE obtained via correspondence analysis. In the end, a comparative study of this method and the method presented by Avron and his collaborators is given.
Добавил в систему: Петрухин Ярослав Игоревич

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

ИСТИНА

ИСТИНА ИНХС РАН

Correspondence analysis and automated proof-searching for first degree entailmentстатья