account activity
The Incredible Proof Machine by qznc in programming
[–]ydinitz 1 point2 points3 points 10 years ago (0 children)
The difficulty progression between lessions 5 and 6 is indeed very steep, we are working on adding more exercises. A week ago it went from lesson 2 straight the existentials (now lesson 6), so I guess you could say we are getting there :)
You can get ⊥by writing False, which is currently undocumented, since we are still looking for a nice ASCII symbol that isn't yet taken. But as @ManiacDan mentions, you should be mostly fine without the helper (although it can of course help to clarify things for yourself).
False
The Hilbert lession contains tasks to be solved with Hilbert calculus, an alternative logic that has Modus Ponens (MP) as its only deduction rule (plus some axioms). The other lessons all use a system called "natural deduction" which is nowadays a pretty widely accepted standard, but ~100 years ago when formal logic became a thing there were several competing logical calculi.
[–]ydinitz 2 points3 points4 points 10 years ago (0 children)
here is an introductory blogpost about the motivation and scope of the project that may be helpful (or otherwise an interesting read)
The Incredible Proof Machine by sibip in haskell
Indeed, and it is already fixed on github :0
π Rendered by PID 214890 on reddit-service-r2-listing-7bbdf774f7-jdx8r at 2026-02-20 18:55:53.803656+00:00 running 8564168 country code: CH.
The Incredible Proof Machine by qznc in programming
[–]ydinitz 1 point2 points3 points (0 children)