<< Prev | - Up - |
Exercises for the chapter on the model checker
Exercise 2.1
[Theoretical Exercise]
Give the set theoretic description of the models that the Prolog lists in Section 2.1.4 and Section 2.1.5 represent.
Exercise 2.2
Write a predicate
wff/1
. It should succeed if and only if its first argument represents a well formed formula over the vocabulary in the database. Thus given our example vocabularysignature.pl
,wff(exists(x, moron(x) & therapist(mary)))
should succeed, while
wff(hate(peter,cinderella)).
should fail, as should:
wff(love(mary)).
[Hint: Use
=..
orcompose/3
fromcomsemLib.pl
to split terms into functor and arguments.]Does your predicate (correctly) require quantifiers to bind variables, i.e. does it rule out formulae like
exists(mary,moron(mary))
? If it doesn't, try to repair it. What does your predicate do if you replace subformulae in its input by Prolog-variables (e.g. if you checkmoron(mary)& X
)?Use your predicate to complete the revised version of our model checker.
Exercise 2.3
Can your predicate
wff/1
be used to generate formulae over a vocabulary by leaving the first argument uninstantiated? Explain your observations.
Exercise 2.4
Write a predicate
wffList/1
that takes a list of formulae and succeeds if and only if all formulae on the list are well formed over the vocabulary in the database.
Exercise 2.5
We did not do anything to make sure that first order variables and constant/predicate-symbols are really distinct. Write a predicate that looks at the database and gives a warning if any first order-variable is also a constant/predicate-symbol.
Exercise 2.6
Write a Prolog program which when given a list of terms, determines whether or not the list represents a model. That is, your program should check whether:
Its input is a list.
All members of this list are well-formed atomic formulae over the given vocabulary.
None of these atomic formulae contains a free variable.
If you've solved Exercise 2.2 or Exercise 2.4, you may be able to reuse parts of the code with minor changes.
Exercise 2.7
[Theoretical Exercise (OPTIONAL)]
We say that two sentences
and
are logically equivalent if and only if
and
. Show that
and
are logically equivalent.
Exercise 2.8
Go through Section 2.1.9. Run the model checker and use
trace/0
to have a look at what the program really does. (The use oftrace/0
is discussed in Practical Session 2 of Learn Prolog Now!).What does the first version of the model checker do if its input formula contains Prolog-variables? Compare e.g. the following calls:
Obviously, the behaviour of the program isn't very consistent (in the last example, the model checker wouldn't come back at all on its own, but our web interface has a timeout of 3 seconds). Find out what's going on and why. Does it make a difference to use the revised
rev_evaluate/2
instead ofevaluate/2
?We ask you to use the ILIAS newsgroup to discuss your findings from Section 2.1.9, as well as any problems you may have in understanding and using the model checker.
Exercise 2.9
[For the code to work, you need a predicate
wff/2
. If you haven't solved Exercise 2.2, tell us and we will send you the code you need.]If our revised model checker is called with an input that is not well-formed or that contains free variables, it will say
no
. As we've discussed, this response is not yet what we'd like to have. Modifyrev_evaluate
so that it distinguishes between non well-formed input and well-formed input that is false in the given model. Non-wellformed input should produce a message and should not be evaluated.
Exercise 2.10
[This is a possible mid-term project]
The definition of truth can be extended from sentences to arbitrary first-order formulae as follows: An arbitrary first-order formula
is true in a model
iff there is an assignment
in
such that
. Remember that for sentences we required that every assignment satisfied the sentence in the given model, but only to find out that assignments didn't matter for satisfying sentences anyway. This time the assignment does matter, because our formula may contain free variables. But we only require that some assignment do the job.
Change the model checker so that it checks if an arbitrary first order formula is true in a model according to our new definition. You will probably have to add an argument that represents a (partial) variable assignment. This argument can then be used by all clauses of the model checker that deal with assigning or instantiating variables. You may use the predicate
subst/3
fromsubstitute.pl
.
<< Prev | - Up - |