«up»

Prolog and First-Order Logic

Abstract:
We would like to use first order logic as a semantic representation formalism, and we want to deal with it in Prolog. So obviously the first thing we need is a way of representing in Prolog the basic entitities that play a role in first order logic. We've seen that these are ↗first-order models, ↗first-order formulae and ↗vocabularies. The first part of this lecture discusses the Prolog representations we will choose for them.Then, we turn to the notion of ↗truth in a model. We approach this notion in Prolog by implementing a simple first-order model checker (or semantic evaluator). The model checker takes a ↗first-order formula and an (exact) ↗first-order model as input and checks whether the formula is true in the model.

Table of Contents

A Simple Model Checker
In this part of the lecture, we'll write a first version of our model checker. This will turn out to be quite easy, but the implementation will still have various shortcomings. (In the second part of the lecture, we will fix the more obvious ones.) How should we implement a model checker? We have four principal tasks: So, let's start.

Refinements
By simply translating some of the theory about first order logic and its semantics (» First-Order Logic) into Prolog, it was easy to implemement a model checker that can already do a lot of nice things. Yet it has its problems, and they will force us to invest some more thought. Let's see what happens if the input differs in various ways from what we've anticipated.

File Listing
All you need for this Chapter..


Exercise

  1. [Theoretical Exercise]
    Give the set theoretic description (» First-Order Models) of the models that the Prolog lists in » Representing Models and » Another Example represent.
  2. Write a predicate wff/1. It should succeed if and only if its first argument represents a well formed formula (» Building Formulae) 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 (» 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.
  3. Can your predicate wff/1 be used to generate formulae over a vocabulary by leaving the first argument uninstantiated? Explain your observations.
  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.
  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.
  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 » Beispiel: EX EX.WFFEX_EX.WFF or » Beispiel: EX EX.WFFLISTEX_EX.WFFLIST, you may be able to reuse parts of the code with minor changes.
  7. [Theoretical Exercise (OPTIONAL)]
    We say that two sentences ϕ and ψ are logically equivalent if and only if ϕ⊧ψ and ψ⊧ϕ. Show that ∀xϕ and ¬∃x¬ϕ are logically equivalent.
  8. Go through » Checking Models. 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:
    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 » Checking Models, as well as any problems you may have in understanding and using the model checker.
  9. [For the code to work, you need a predicate wff/2. If you haven't solved » Beispiel: EX EX.WFFEX_EX.WFF, 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.
  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 M iff there is an assignment g in M such that M,g⊧ϕ. 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 (» substitute/4) from substitute.pl .
«up»