Decision procedure

A decision procedure is a test for theoremhood in a formal system which is guarenteed to terminate in a finite amount of time. If the string in question is produced; when that happens, you know it is a theorem-and if it never happens, you know that it is not a theorem. When you have a decision procedure, then you have a very concrete characterization of the nature of all theorems in the system.

---

References

Metadata

Type: Tags: Status:⛅️