Formally Verifying Dynamic Properties of Knowledge Based Sys(9)

Abstract. In this paper we study dynamic properties of knowledge-based systems. We argue the importance of such dynamic properties for the construction and analysis of knowledge-based systems. We present a case-study of a simple classification method for w

filter-trace#(cs;vartrace,output)

begin

/thenifcs=0

/;trace:=nilendbeginoutput:=0

else

varcandidate=select(cs)in

begin

ifcorrect(candidate)then

begin

filter-trace#(cscandidate;trace,output);

output:=insert-class(candidate,output)

end

else

begin

filter-trace#(cscandidate;trace,output);

end

trace:=candidate::trace

end

end

Fig.3.Versionofthelinear lteringPSMwhichcomputesatrace

function,namelythattheclassesoftheinputareselectedusingaheuristicfunctionwhichselectstheclasswiththehighestheuristicvalue.

ccsmeasurecmeasureselectcs

Theadaptedfilter-trace#programhastwooutputparameters:traceandoutput.However,inaspeci cationafunctioncanonlyreturnoneoutput.Thistechnicalobsta-clecanbeavoidedbyintroducingtwoauxiliaryprograms:oneprogramforreturningthetraceparameter,andoneforreturningtheoutputparameter.Thetrivialimple-mentationoftheseauxiliaryprogramsisasfollows:

filter-trace-1#(cs;varoutput)

begin

vartrace=nilin

filter-trace#(cs;trace,output)

end

filter-trace-2#(cs;vartrace)

begin

/invaroutput=0

filter-trace#(cs;trace,output)

end