PROBLEM-ORIENTED KNOWLEDGE BASES AND THEIR APPLICATION IN THE PROGRAMVERIFICATION SYSTEM SPEKTR

Citation
Va. Nepomnyashchii et Aa. Sulimov, PROBLEM-ORIENTED KNOWLEDGE BASES AND THEIR APPLICATION IN THE PROGRAMVERIFICATION SYSTEM SPEKTR, Journal of computer & systems sciences international, 36(2), 1997, pp. 321-327
Citations number
9
Categorie Soggetti
Controlo Theory & Cybernetics","Computer Science Theory & Methods","Computer Science Artificial Intelligence","Computer Science Cybernetics
ISSN journal
10642307
Volume
36
Issue
2
Year of publication
1997
Pages
321 - 327
Database
ISI
SICI code
1064-2307(1997)36:2<321:PKBATA>2.0.ZU;2-J
Abstract
The notion of the knowledge base is discussed within the framework of the problem-oriented approach to the program verification. A knowledge base consists of axioms represented by generalized condition term rew riting rules, strategies of their application, and decision procedures . The standard form of axioms is extended by conditions in premises an d in the built-in, case-based reasoning. A survey of knowledge bases o f sorting and compiling programs is given. The verification system SPE KTR is described, where the evidence of correctness is automatically s hown with the use of knowledge bases.