Что такое естественный вычет используется за пределами академии?

Question

Я изучаю естественную дедукцию как часть моего курса по информатике в университете / колледже.

Мне это интересно, но я гораздо лучше учусь, когда могу найти практическое применение вещам.

Может ли кто-нибудь объяснить мне, если и как естественный вывод используется, кроме как для формальной проверки битов кода?

Спасибо!

Answer 1

Естественный вывод не так широко используется в практических формальных методах: последовательное исчисление обычно является лучшей основой, поскольку оно ближе к методам таблиц, используемым при построении процедур принятия решений для логики. Табличные методы довольно важны для практического применения логики в информатике.

Естественная дедукция наиболее часто используется в конструктивной теории типов, и это дает ей некоторые рычаги при проектировании языка программирования. Это считается хорошо знать, а не обязательно знать.

Основная ценность естественного вывода заключается в том, что это самый хороший способ выучить формальный умозаключение, но это дидактическое приложение, встречающееся в основном в академических кругах.

Answer 2

Естественная дедукция очень интересная и довольно крутая, но она очень редко используется вне академических кругов. Формальные доказательства корректировок в программах утомительны с использованием естественных дедукций, и поэтому часто используются инструменты более высокого уровня.