Encoding Input Files

Input file formats (for belief change scenarios) vary according to the list (KB, Revision, Contraction, EB IC, or CB IC) to which formulas are to be added. Any KB file to be loaded should precede each knowledge base by a line ``KB :" (without the double quotes) and list each formula on a separate line. Each formula is listed on a separate line in any Revision and EB IC input files. For any contraction and CB IC input files, each line is interpreted as an independent formula for contraction and as a CB IC, respectively.

Consider an example contraction file. While the formula

(p&~q)

means that $(p\&\neg q)$ is to be removed from the consequences of the resulting knowledge base,

p

~q

listed on two seperate lines means that both $p$ and $\neg q$ are to be dropped from the consequences of the resulting knowledge base.

As an example, Table 3 shows some valid input files.

Table: Example Input Files

KB	Rev	Cont	EB IC	CB IC
KB :	q	p	(a&b+c)	d
(p&q&r)	~p	~q	(x&(y+z))	~d
(~q+~s)