User Tools

Site Tools


exam

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
exam [2011/07/13 15:14]
131.246.18.253
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?​ 
 + 
 +:?: How does the automatic proof of termination work for //​definition//,​ //​primrec//,​ and //fun//? 
 + 
 +:?: What is the general procedure for proving termination manually in //​function//?​
 ===== Calculi ===== ===== Calculi =====
  
 :?: 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.1310562854.txt.gz · Last modified: 2011/07/13 15:14 by 131.246.18.253