The Logic of and

    In this section we give the properties of the functions and , which are central for representing question/answer discourses. Since the and functions are treated in the style of situation calculus, we do not need to change our basic theory of context, but simply give the axioms that formalize the two functions.

Intuitively, the function will set up a context in which the reply to the question will be interpreted. For example, the context resulting in asking some proposition p will have the property that in that context will be interpreted as p. Thus only changes the semantic state of the discourse context. The function will do a simple update of information: the formulas true in the context resulting in replying p in will be exactly those formulas which are conditionally true on p in . Thus the function only changes the epistemic state of the discourse context. We now make these notions more precise.

The following axioms characterize the functions and .

interpretation axiom (propositional)

if is a closed formula, then

frame axiom (propositional)

if is a closed formula, and does not occur in , then

interpretation axiom (qualitative)

if x is the only variable occurring free in , then

frame axiom (qualitative)

if x is the only variable occurring free in , and does not occur in , then

reply axiom

The predicate is used to return an answer to a qualitative question, similar to the way it is commonly used to return a witness in a resolution theorem prover; see [27].

We proceed to illustrate the axioms and their use with an example.