What is natural deduction used outside of academia?

I study natural deduction as part of my formal specification and verification course at a university / college.

It is interesting to me, but I will learn much better when I can find practical application for things.

Can someone explain to me if and how natural inference is used, other than formal verification of code bits?

Thanks!

+4
source share
3 answers

Natural deduction is not used much in practical formal methods: sequential calculus, as a rule, is the best basis, since it is closer to the table methods used in constructing decision-making procedures for logic. Table methods are quite important for the practical application of logic in computer science.

Natural deduction is most often used in the theory of a constructive type, and this gives it some advantage in the development of a programming language. He believed that he was well acquainted, and should not know.

The primary importance of natural deduction is that it is the finest way to study formal derivation, but it is a didactic application, considered mainly in academic circles.

+3
source
The natural conclusion is very interesting and classy, ​​but it is very rarely used outside the academic community. Formal evidence of program correction is tedious using natural deduction, so higher-level tools are often used.
+1
source

Should I cross the road here?

  • Passes a big bus.
  • On the road is lava.
  • Ahead is another 10 meters.

Conclusion: do not cross the road here.

-4
source

Source: https://habr.com/ru/post/1306609/


All Articles