Department information

 

Accommodative Belief Revision - Implementation

The paper "Accommodative Belief Revision" by Satu Eloranta, Raul Hakli, Olli Niinivaara, and Matti Nykänen (accepted for publication in JELIA'08) describes a novel approach to belief revision. It also describes a prototype implementation for trying out the approach.

This page lets you download this implementation and gives a short guide on how it it used, assuming that you have read the paper itself.

If you have any questions regarding the implementation or this guide, please e-mail their author Matti Nykänen at matti.nykanen@cs.uku.fi.

Haskell

It is also assumed that you already know how to start a Haskell interpreter, and how to load the downloaded source file OCF.hs into it. It was developed using GHCi (version 6.8.2) but should work in other interpreters as well.

Knowledge Expansion Command

The implementation is a library of data types and functions. The central data type is the OCF (Ordinal Conditional Function) as described in the paper, while the functions let you refine a given OCF into another by given a logical formula. Let us start with the OCF refining commands, and defer the syntax of these formulas for later.

One way to refine a given OCF is by giving the command

*OCF> new <- know old formula

where

old

is the Haskell variable name for the existing OCF. The implementation predefines one such variable, namely the initialOCF described in the paper.

new

is the Haskell variable name for the OCF obtained by refining the knowledge in old to include also this formula. Then you can use this new name in subsequent commands. You can also leave out the new <- part, if you don't need a name for the result; the interpreter lets you refer to the last OCF obtained via the special variable named it.

If this formula contradicts the knowledge in old, then you get the error message

*** Exception: The OCF assumptions are contradictory!

but otherwise the interpreter will display the new OCF using the current syntax described below.

Belief Revision Command

Another way to refine a given OCF is by giving the command

*OCF> new <- operator old formula

which performs the accommodative belief revision described in the paper using one of the following:

operator	suggested by
hearB	Borgida
hearD	Dalal
hearS	Satoh
hearW	Weber.

If the given formula agrees with the knowledge in the old OCF, then the implementation responds with

I will believe the following:
	believed

where believed is the formula which describes the beliefs in the new OCF. It is displayed using the default syntax explained below.

But if they do not agree, then the response is instead

I will not believe that! Instead I will believe the following:
	believed

where the given formula is first forced to agree with the knowledge via the chosen operator.

In both cases, the new OCF is also displayed using the current syntax explained below.

Formula Syntax

The commands described above take their formulas as strings enclosed in double quotes: "..."". This string can contain whitespace, which is ignored.

A propositional symbol is written like an identifier in a programming language: as a word which starts with a letter and continues with letters and numbers. These words are case-sensitive.

The implementation offers the following logical connectives, where A and B are formulas:

notation	connective
-A	negation
A&B	conjunction
A|B	disjunction
A=>B	implication
A<=>B	equivalence

Explicit parentheses (...) can be used in formulas. If they are not used, then the earlier connectives bind tighter than the later ones in the list above. Thus for instance writing "x|-y&z" is permitted and means "x|((-y)&z)" and so on. Hence the common conventions on omitting parentheses apply here as well.

Display Syntax

The default syntax for displaying an OCF is by displaying entries

rank : formula

which means that all the worlds which received exactly this rank are described by that formula. These entries are displayed by ascending rank for each finite rank given to some world. The formula is given in Disjunctive Normal Form (DNF) in the formula syntax with each disjunct as its own line.

The command byGrove switches from this default syntax into one where the formula describes instead the worlds which received at most this rank. The command bySpohn reverts back into the default syntax.

The command byWorld switches from the current syntax into displaying the truth table of the formula instead. Only the true rows are displayed, each as its own line. The proposition symbols are displayed as the table header, where their names are now written down instead of the usual left-to-right direction.

If you write

*OCF> name

then the implementation will display the named OCF using the current syntax.

Note finally that displaying a named OCF or giving a by... command resets the variable named it. Thus it might be a good idea to give it an alias first:

*OCF> let alias = it