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 vocabulary signature.pl ,

wff(exists(x, moron(x) & therapist(mary)))

should succeed, while

wff(hate(peter,cinderella)).

should fail, as should:

wff(love(mary)).

comsemLib.pl: View Download

[Hint: Use =.. or compose/3 from comsemLib.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 check moron(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 of trace/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:

• evaluate(X,1).

• evaluate(moron(peter) v X,1).

• evaluate(X & moron(mary),1).

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 of evaluate/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. Modify rev_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 from substitute.pl .