3 ms·
This is sufficient for theorem-proving work. Compare and contrast Metamath, which also requires users to define their own syntax and rewrite rules, and cannot d
by lidHanteyk 7y ago
This is sufficient for theorem-proving work. Compare and contrast Metamath, which also requires users to define their own syntax and rewrite rules, and cannot do proof search. Nonetheless, this minimal functionality is enough.
- seanmcdirmid 7y agoTo me, theorem proving is automated reasoning, whereas here the system focuses on making human directed reasoning more efficient. The line is a fine one, I guess.