There's a lot of theory involved in automated reasoning, but why not represent things with any old OOP hierarchy that makes sense?

Do I need to learn another area of math to make something that functions?

  • 2
    $\begingroup$ No, but automated proving is usually done in a constructive setting and constructive mathematics is easier with types than with ZFC. $\endgroup$ – neptun Nov 18 '17 at 22:30
  • 3
    $\begingroup$ Note also that the type systems of object oriented programming basically is a variant of type theory, and the versions that make sense to do mathematics are usually known by mathematical names. $\endgroup$ – neptun Nov 18 '17 at 22:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.