Вікіпедія

Теоретико-доказова семантика: відмінності між версіями

Інтерактивний перегляд історії
[неперевірена версія][неперевірена версія]
← Попереднє редагуванняНаступне редагування →
Вилучено вміст Додано вміст
ВізуальнийВікірозмітка
Немає опису редагування
Мітки: Редагування з мобільного пристрою Редагування через мобільну версію
Немає опису редагування
Мітки: Редагування з мобільного пристрою Редагування через мобільну версію
Рядок 5:
[[Даг Правітц]] поширив поняття Генцен на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] і [[теорія типів|інтуїтивної теорії типів]]. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантику доказу.
 
[[Майкл Дамм]] представив дуже фундаментальну ідею [[логічна гармонія|логічної гармонії]], спираючись на пропозицію [[Нуель Белнап]]. Коротше кажучи, мова, яка, як розуміється, пов'язаний з певними шаблонами виведення, має логічну гармонію, якщо завжди можна відновити аналітичні докази від довільних демонстрацій, що можна показати для секвенційного обчислення за допомогою теорем виключення вирізу і Для природного виведення за допомогою теорем нормування. Мова, в якому відсутня логічна гармонія, буде страждати від наявності некогерентних форм виведення: це, ймовірно, буде непослідовним.
 
Посилання
Отримано з https://uk.wikipedia.org/wiki/Теоретико-доказова_семантика