4 ms·

I'm not so sure, because Prolog.

• anon291 8mo ago
  Prolog is not a theorem prover. Theorem provers are total (I.e. not turing complete)
  • cess11 8mo ago
    "Is Prolog a theorem prover? Richard O'Keefe said it best: Prolog is an efficient programming language because it is a very stupid theorem prover." https://www.metalevel.at/prolog/theoremproving https://www.metalevel.at/prolog/theoremproving Who am I to overrule the author of The Craft of Prolog? Some would say that SLDNF resolution qualifies as theorem proving, some would disagree and say that a theorem prover also needs such and such capability. Anyway, as Triska shows above you can implement software that is quite a lot like a theorem prover in about thirty lines of Prolog, i.e. not "a dependently typed functional programming language". The descendants of Milner's work, notably ML and the Edinburgh LCF theorem prover, have been quite successful, though.