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/06/10 11:56]
131.246.41.159 [Exam Questions]
exam [2011/08/02 15:29] (current)
188.107.127.174 [Core HOL]
Line 25: Line 25:
  
 :?: What is Specification?​ :?: What is Specification?​
-  * defining all possible behaviours of the specified ​syetsm+  * defining all possible behaviours of the specified ​system 
 + 
 +:?: What is the difference between model- and property-oriented specifications?​ 
 +  * Model-oriented is based on well-defined mathematical objects like sets and functions, which are used to construct a representation of the system state, as well as the operations on these states. Thus, such specifications reason about a transition system. 
 +  * Property-oriented is purely declarative. It uses some logic language to express the properties of the functions in the system. 
 :?: What is a Model? :?: What is a Model?
 ===== Core HOL ===== ===== Core HOL =====
Line 36: 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.
 +
 +:?: How can we prove formulas without a calculus?
 +  * Calculi are based purely on syntax. We can always rely on semantic proofs, e.g. truth table or tableaux methods.
exam.1307699811.txt.gz · Last modified: 2011/06/10 11:56 by 131.246.41.159