Coq and Agda are automated theorem provers that use dependently typed lambda calculus as a basis
https://ru.wikipedia.org/wiki/Автоматическое_доказательство
Процесс доказательства основывается на логике высказываний и логике предикатов.
после полной автоматизации доказательство называют уже "вычислением".
В настоящее время автоматическое доказательство теорем в промышленности применяется в основном при разработке и верификации программного обеспечения.
Корпорация Microsoft использует автоматический доказатель теорем Z3 для верификации кода операционной системы Windows и других программных продуктов
The typed lambda-calculus is a formulation of higher-order logic well suited to the formalization of mathematics and other disciplines.
one can search for a proof of a theorem of typed lambda-calculus by searching for an expansion proof which expresses the fundamental logical structure of the theorem, and then transform this into a proof in natural deduction style.
https://en.wikipedia.org/wiki/Prolog
There is currently a great deal of research into lambda calculus by the programming language, theorem proving and symbolic computing communities.
https://www.math.cmu.edu/math/faculty/StatmanRichard
mathematical expressions and statements can be modeled using lambda calculus.
The lambda calculus is also a logic. It was originally created to solve one of the many early formulations of the halting problem. It turned out, though, that the raw untyped lambda calculus allowed for unrestricted recursion (the fixedpoint combinators), making it unsuitable for logic (turing completeness in a logic makes your logic inconsistent. The liar's paradox is just an infinite loop).
To fix this problem, Church revised the lambda calculus, adding types to it. The "simply typed" lambda calculus restrict the expressivity of the language severely, but kept it consistent.
(Специально для Уткина - количество использованного английского языка является индикатором уровня моего непонимания вопроса. Чем лучше понимаю, тем больше обхожусь своими словами)
Отредактировано Лис (2018-01-30 18:48:00)
.