Timeline for Computational complexity of proof verification
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 12, 2020 at 18:02 | comment | added | Arno | Yes, for those examples deciding the axioms is easy. Take for instance ZFC. There are finitely many special axioms, and then the axioms schema replacement and separation. Checking whether a given formula is an instace of the schema is just a pattern-matching issue. | |
| Jul 12, 2020 at 17:52 | comment | added | jg1896 | Thank you very much. This is great. Since you pointed out, and I neglected, if we consider some canonical axiom system (ZFC, PA, Groups, modules, etc), the axioms can be decided polynomially, right? | |
| Jul 12, 2020 at 17:49 | vote | accept | jg1896 | ||
| Jul 12, 2020 at 17:43 | history | answered | Arno | CC BY-SA 4.0 |