Inproceedings610: Unterschied zwischen den Versionen
K (Added from ontology) |
K (Added from ontology) |
||
Zeile 1: | Zeile 1: | ||
+ | {{Publikation Author | ||
+ | |Rank=1 | ||
+ | |Author=Dieter Fensel | ||
+ | }} | ||
+ | {{Publikation Author | ||
+ | |Rank=4 | ||
+ | |Author=Bob Wielinga | ||
+ | }} | ||
{{Publikation Author | {{Publikation Author | ||
|Rank=2 | |Rank=2 | ||
Zeile 6: | Zeile 14: | ||
|Rank=3 | |Rank=3 | ||
|Author=Rix Groenboom | |Author=Rix Groenboom | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
}} | }} | ||
{{Inproceedings | {{Inproceedings |
Version vom 15. August 2009, 22:54 Uhr
Specification and Verification of Knowledge-Based Systems
Specification and Verification of Knowledge-Based Systems
Published: 1996
November
Buchtitel: Proceedings of the 10th Banff Knowledge Acquisition for Knowledge-Based Systems Workshop (KAW-96), Banff, Canada, Novemver 9-14, 1996
Referierte Veröffentlichung
BibTeX
Kurzfassung
The paper introduces a formal approach for the specification and verification of knowledge-based systems. We identify different elements of such a specification: a task definition, a problem-solving method, a domain model, an adapter, and assumptions that relate these elements. We present abstract data types and a variant of dynamic logic as formal means to specify these different elements. Based on our framework we can distinguish several verification tasks. In the paper, we discuss the application of the Karlsruhe Interactive Verifier (KIV) for this purpose. KIV was originally developed for the verification of procedural programs but it fits well for our approach. We illustrate the verification process with KIV and show how KIV can be used as an exploration tool that helps to detect assumptions necessary to close the gap between the task definition and the competence of a problem-solving method.
Download: Media:1996_610_Fensel_Specification_a_1.ps.gz
Weitere Informationen unter: Link