User Tools
exam
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
exam [2011/07/13 15:18] 131.246.18.253 [Core HOL] |
exam [2011/08/02 15:29] (current) 188.107.127.174 [Core HOL] |
||
|---|---|---|---|
| Line 41: | Line 41: | ||
| :?: How are the elements //True// and //False// introduced in HOL? | :?: How are the elements //True// and //False// introduced in HOL? | ||
| - | * Since there should always be an infinite set in **U** whose elements and power sets are also fully contained in **U**, there's a guarantee that there will be a set with two elements and that set is going to represent the values //True// and //False// ((Did I miss something?)) | + | * Since there should always be a distinguished infinite set in **U** whose elements and subsets are also fully contained in **U**, there's a guarantee that there will be a set with two elements (say the subset {0,1} of the infinite set) and that one is going to be mapped further on to the values //True// and //False// ((Did I miss something?)) |
| :?: Why must all functions be total in Isabelle/HOL? | :?: Why must all functions be total in Isabelle/HOL? | ||
| Line 51: | Line 51: | ||
| :?: Why do we need calculi. | :?: Why do we need calculi. | ||
| + | * Basically, calculi are the tools we use to derive (and prove) theorems. Given a set of valid formulas and a sound calculus, new valid formulas (tautologies) can be derived. As far as I know, the semantic notion of "validity" corresponds to "provability" in the calculus, since it does not consider any notion of "truth". | ||
| :?: Please explain the following properties: Soundness (Correctness), Completeness, ... | :?: Please explain the following properties: Soundness (Correctness), Completeness, ... | ||
| + | * A deductive system is sound if all provable formulas are valid. It is complete if all valid formulas are provable. | ||
| + | * Validity is a semantic property ($A \models B$), while provability a syntactic one ($A \vdash B$). So, in other words we have: | ||
| + | * Soundness: $A \vdash B \longrightarrow A \models B$ | ||
| + | * Completeness: $A \models B \longrightarrow A \vdash B$ | ||
| :?: What are the advantages/disadvantages of the Hilbert calculus compared to the Gentzen calculus. | :?: What are the advantages/disadvantages of the Hilbert calculus compared to the Gentzen calculus. | ||
exam.1310563085.txt.gz ยท Last modified: 2011/07/13 15:18 by 131.246.18.253
Page Tools
