2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




 
 Преобразования генценовских формализмов в гильбертовские
Сообщение29.01.2017, 18:36 
Хотелось бы просто ссылку на литературу. Это уж точно где-нибудь в полноте расписано. Конкретнее, интересует натуральная дедукция, а sequent calculus, хотя в принципе и интересует немного тоже, но в практической задаче формулировки именно в первом виде.

Заранее спасибо, конечно же. :-)

 
 
 
 Re: Преобразования генценовских формализмов в гильбертовские
Сообщение18.10.2019, 22:26 
[Time skip]

Кому интересно, я потом от этого стремления ушёл. Мне нужно было просто записывать натуральную дедукцию более скромно, линейно, а это можно устроить, используя старых добрых Карри—Говарда, собирая выводы некой штуки в соответствующий тип и конкретным выводам сопоставляя терм-значение, а выводам из гипотез $\gamma_1,\ldots,\gamma_n$ — термы вида $\lambda\gamma_1.\cdots\lambda\gamma_n.t$, ну и т. д., получается какая-нибудь теория типов. Гипотетические выводы в посылках меня только и путали.

 
 
 [ Сообщений: 2 ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group