3 ms·
A theorem prover is a dependently typed functional programming language. If you can generate a term with a particular type then the theorem is true. There is no
by anon291 8mo ago
A theorem prover is a dependently typed functional programming language. If you can generate a term with a particular type then the theorem is true. There is no testing involved.
- cess11 8mo agoI'm not so sure, because Prolog.
- anon291 8mo agoProlog 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.
- nextos 8mo agoThere are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.
- anon291 8mo agoWeakly typed, but strongly kinded. It is a strict requirement that all theorem provers have a notion of type. This is by contradiction. Suppose you had a weakly typed theorem language L. Suppose you have a definition D of set in this weakly typed theorem language. Then say x is a set by D. Now suppose y is the set in D of all sets in D that do not contain themselves (Russell...). If this construction were allowed then the theorem prover is not a theorem prover. If this construction is rejected then the theorem prover has a strict notion of kinds of sets which means it's not weakly typed. Mizar and such do not require constructive definitions a la coq but it has to stratify its universes.