Computational Logic

Ga naar: navigatie, zoeken

Samenvattingen

Klik hier om de samenvattingen te bekijken

Voorbeeld Examenvragen

Voorbeeld examenvragen voor het vak Computational Logic (zoals die te vinden zijn op [[1]], verkregen op 09/06/2012):

1. (20 minutes) Consider the following clausal theory (variables start with capital):\\ .....

  • a. Using the two element domain $\{0,1\}$, carefully construct an interpretation of the above theory and compute the truth of the clauses. If feasible, choose an interpretation which is a model for the clausal theory (do not spoil your time in searching an interpretation that is a model).
  • b. Assuming the existence of a model for the above clausal theory, what can you say about the existence of an SLD-refutation for the logic program consisting of the clauses ... under the query ...
  • c. Draw an SLD-tree for this logic program and query.

2. (10 minutes) Apply the Paterson-Wegman unification algorithm (the one using directed acyclic graphs to represent terms) to unify the following pair of terms (variables start with capital): ...

3. (10 minutes) Give the more general relation between the following three terms (variables start with capital): ...; give the more general relation between the following three substitutions: ...

4. (10 minutes) Construct the completion of the following program: ...

5. (60 minutes) Consider the program: ...

  • a. Is the program stratified? If so compute its perfect model.
  • b. Compute for this program the least fixpoint of $\Phi_P$, the Fitting operator based on three valued logic.
  • c. Show an SLDNF-tree for the goal ...
  • d. Show an SLDNFtree for the goal ... when calls to ... are tabled.
  • e. What is the truth of ... when considering the program as an inductive definition? And under the well-founded semantics? Reuse results from previous points if useful.
  • f. Verify whether the set of atoms true in the fixpoint computed for (b.) is a stable set (a stable model).
  • g. Assume the predicate ... is not defined but open (or abducible), and the integrity constraint ... is added. Show an abductive SLDNF-tree for the query ...

6. (60 minutes) Consider the program: ...

  • a. Abstraction of terms: ... Construct either an abstract OLDT-tree or an abstract LSLDT-tree for the abstract goal ... Collect the abstract call patterns from the constructed tree.
  • b. Define $lenght(t)$ as ... Verify that answers ... satisfy the property ....
  • c. Proof that the program is left terminating for goals abstracted by ..... Make clear which approach you follow. If relevant for the approach you follow, reuse parts of (a.) and (b.).

7. (30 minutes) Consider the program: ... Use conjunctive partial deduction to specialise this program for goals of the form ....