User Tools
faq
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
faq [2012/04/16 16:40] paddy [Programming Language Semantics] |
faq [2012/04/16 22:38] 95.89.150.111 [PURE vs. HOL] |
||
|---|---|---|---|
| Line 202: | Line 202: | ||
| :!: There are several levels to this question: | :!: There are several levels to this question: | ||
| - | - First, the latter is a by itself a HOL formula, while the former contains HOL formulas, but is more considered a rule. | + | - First, the latter is by itself a HOL formula, while the former contains HOL formulas, but is more considered a rule. |
| - The former says that $G$ can be proven //syntactically// from the given assumptions $A_1, A_2, A_3$. The latter says that you can prove using no assumptions that whenever all $A_1, A_2, A_3$ hold, $G$ holds, too. | - The former says that $G$ can be proven //syntactically// from the given assumptions $A_1, A_2, A_3$. The latter says that you can prove using no assumptions that whenever all $A_1, A_2, A_3$ hold, $G$ holds, too. | ||
| - Maybe the main practical difference: the former is nicely applicable as a rule, where the latter is nearly useless. | - Maybe the main practical difference: the former is nicely applicable as a rule, where the latter is nearly useless. | ||
faq.txt ยท Last modified: 2013/03/01 10:12 by 124.207.188.66
Page Tools
