что такое "cut-free Gentzen ..." ?

[Levon11]

Добрый день Всем!

Мне нужно разобраться в статье на английском языке. Помогите перевести заглавие.

Tractability of cut-free Gentzen type propositional calculus with permutation inference

Я это перевел так

Трактовка "cut-free Gentzen" типа пропозиционального исчисления c перестановкой
(вывода, умозаключения; следствия)

Но я так и не понял что такое "cut-free Gentzen type"....

[Someone]

Levon11 писал(а):

Но я так и не понял что такое "cut-free Gentzen type".... :?:

свободного от сечения генценовского типа

[Levon11]

Спасибо.

А что такое сечение генценовского типа?

[Someone]

Levon11 писал(а):

Спасибо.

А что такое сечение генценовского типа?

Я думаю, что тут "скобки" нужно поставить иначе. Термины "свободное от сечения" и "генценовского типа" - это определения к "пропозициональному исчислению". Что это такое - ищите в литературе, я не специалист в этой области. Чтобы Вам объяснить, мне придётся сначала самому разобраться.

[Levon11]

Ясно.

[Yuri Gendelman]

Я бы перевел "cut-free Gentzen type propositional calculus" как "исчисление высказываний Генценовского типа без отсечений".
Судя по названию, статья посвящена теории сложности выводов в логических исчислениях.

[Someone]

Скорее всего, нет. Дело в том, что сечение - это правило вывода

$$\frac{\Gamma\cup\{\varphi\}\quad\Gamma\cup\{\neg\varphi\}}{\Gamma}\text{,}$$

где $\Gamma$ - некоторое конечное множество формул.

[Yuri Gendelman]

Да, Вы правы, наверное лучше "...без сечений...".
Я вспомнил, что мне встречалось правило сечения, в виде:

$$\frac{\Gamma \vdash \Phi; \;\; \Phi, \Pi \vdash \Lambda}{\Gamma, \Pi \vdash \Lambda}$$

(сечение по $\Phi$), в контексте автоматического построения вывода теорем.
Насчет теории сложности - это навеяно термином "Tractability".

[luitzen]

…of cut-free Gentzen type propositional calculus with permutation inference = …свободного от сечения пропозиционального исчисления генценовского типа с правилом перестановки.

Tractability, думаю, можно вообще перевести как «полиномиальность».
Ну а так — «обозримость», наверное.

[Yuri Gendelman]

luitzen писал(а):

…of cut-free Gentzen type propositional calculus with permutation inference = …свободного от сечения пропозиционального исчисления генценовского типа с правилом перестановки.
Tractability, думаю, можно вообще перевести как «полиномиальность».
Ну а так — «обозримость», наверное.

tractability = "разрешимость"
inference = "логический вывод" или просто "вывод"

[luitzen]

Yuri Gendelman писал(а):

tractability = "разрешимость"
inference = "логический вывод" или просто "вывод"

К сожалению, все хорошие слова русского языка давно уже заняты. Разрешимость — довольно строгое понятие и используется (в контексте темы «математическая логика») для перевода чего-нибудь наподобие decidability.
Inference — это своего рода сокращение для inference rule, «правило вывода».
В конце концов, обсуждаемая статья доступна для скачивания. Можно скачать и посмотреть, о чём там речь.

P.S. А вот что-нибудь вроде практическая разрешимость для перевода tractability, наверное, подошло бы.