Formally Verifying Dynamic Properties of Knowledge Based Systems(18)

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

ToynatureofourPSMs.Ourexamplesareunrealisticallysmall,andcannotbeusedinrealisticapplications.Forexample,inmulti-classclassi cation(whereananswerscontainsnclasses,insteadofjustone),thenumberofanswer-candidatesgrowthsex-ponentiallywithn.Insuchacase,ourlinear lteringPSMwouldnotbeveryattractive.Nevertheless,webelievethatthesameresultsaspresentedinthispapercanbeobtainedformorerealisticPSM’s.Wearecurrentlyworkingonobtaininganytime-resultsforacollectionofmorerealisticmethodstakenfromastandardKBStextbook[21]

5.2EvaluationofKIV

Ourcase-studywasnotmeantasaseriousevaluationstudyofKIV.Nevertheless,ourexperienceswithKIVhavebeenquitepositive,forthefollowingreasons.Firstly,KIVallowsthehierarchicaldecompositionofthesoftwaresystem(bothspeci cationsandimplementations).Thisachievestheusualadvantagesofmodularity.Furthermore,KIVallowsustoprovepropertiesofhigherlevelfunctionsandprograms(suchfilter#)withouthavingtoprovideimplementationsoflowerlevelprograms,suchasinsertwhichisusedbyfilter#.Instead,onlyaspeci cationoftheselower-levelfunctionsisrequired,abstractingfromtheirimplementationdetails.