4 ms·
How does Prolog relate to more formal languages like Lean/Coq? Prolog (pretty easily) has dependent types [1] as well. Is there something in the language itse
by infogulch 7y ago
How does Prolog relate to more formal languages like Lean/Coq? Prolog (pretty easily) has dependent types [1] as well. Is there something in the language itself that would make it unsuitable as a theorem prover, or is there something it's missing? I'm trying to get a feel for Lean from the vantage of a bit of familiarity with Prolog.
[1]: https://llaisdy.co.uk/2014/05/07/dependent-types-in-prolog/ https://llaisdy.co.uk/2014/05/07/dependent-types-in-prolog/
- agentultra 7y agoI'm not sure I can answer that question. I don't know enough about Prolog. I can say that your example could be encoded in Lean as a type and the definition would probably be much shorter. Does Prolog automate some of the work involved in writing a proof?