|
|
|
|
Show HN: Live software archaeology of FOL (theory of reasoning)
(io.livecode.ch)
|
|
3 points
by namin
379 days ago
|
|
|
I want to share this live playground for FOL, an old system from the late 70s. It has many precursor ideas about reasoning at the meta-level, including the now common proof by reflection which turns proving in the object theory into evaluation in the meta theory, and is common in Rocq, Lean, and other proof assistants. |
|
|