{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T18:29:59Z","timestamp":1767637799656,"version":"3.48.0"},"reference-count":86,"publisher":"Maximum Academic Press","issue":"4","license":[{"start":{"date-parts":[[2009,7,7]],"date-time":"2009-07-07T00:00:00Z","timestamp":1246924800000},"content-version":"unspecified","delay-in-days":4967,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Knowledge Engineering Review"],"published-print":{"date-parts":[[1995,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This paper presents a general discussion of the role of formal methods in knowledge engineering. We give an historical account of the development of the field of knowledge engineering towards the use of formal methods. Subsequently, we discuss the pros and cons of formal methods. We do this by summarising the proclaimed advantages, and by arguing against some of the commonly heard objections against formal methods. We briefly summarise the current state of the art and discuss the most important directions that future research in this field should take. This paper presents a general setting for the other contributions in this issue of the journal, which each deal with a specific issue in more detail.<\/jats:p>","DOI":"10.1017\/s0269888900007554","type":"journal-article","created":{"date-parts":[[2009,7,7]],"date-time":"2009-07-07T09:34:20Z","timestamp":1246959260000},"page":"345-360","source":"Crossref","is-referenced-by-count":16,"title":["Formal methods in knowledge engineering"],"prefix":"10.48130","volume":"10","author":[{"given":"Frank","family":"van Harmelen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dieter","family":"Fensel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"27968","published-online":{"date-parts":[[2009,7,7]]},"reference":[{"key":"S0269888900007554_ref070","first-page":"745","volume-title":"Proceedings of the 11th European Conference on AI (ECAI'94)","author":"Treur","year":"1994"},{"volume-title":"Applications of Formal Methods","year":"1995","author":"Parnas","key":"S0269888900007554_ref058"},{"volume-title":"Knowledge oriented software Design","year":"1993","author":"Angele","key":"S0269888900007554_ref003"},{"key":"S0269888900007554_ref062","unstructured":"Schreiber ATh and Terpstra P , 1995, \u201cSisyphus-VT: A Common KADS solution\u201d Internationalfournalof Human-Computer Studies (in press)."},{"key":"S0269888900007554_ref054","unstructured":"Milnes B , 1992, \u201cA specification of the Soar cognitive architecture in Z\u201d, Technical Report CMU-CS-92\u2013169. Carnegie Mellon University, 08."},{"volume-title":"Communication and Concurrency","year":"1989","author":"Milner","key":"S0269888900007554_ref053"},{"key":"S0269888900007554_ref050","first-page":"83","volume-title":"Proceedings of the Third KADS User Meeting","author":"L\u00f6ckenhoff","year":"1993"},{"volume-title":"Proceedings of the 5th European Software Engineering Conference (ESEC'95)","year":"1995","author":"Landes","key":"S0269888900007554_ref048"},{"volume-title":"Formal Specification of Complex Reasoning Systems","year":"1993","author":"Kassel","key":"S0269888900007554_ref045"},{"key":"S0269888900007554_ref021","unstructured":"Craigen D , Gerhart S and Ralston T , 1993, \u201cAn international survey of industrial applications of formal methods\u201d Technical report, U.S. Department of Commerce, Technology administration, National Institute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD 20899, USA, 03."},{"key":"S0269888900007554_ref051","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900006238"},{"volume-title":"Object-Oriented Programming in Common Lisp","year":"1984","author":"Keene","key":"S0269888900007554_ref046"},{"key":"S0269888900007554_ref042","first-page":"248","volume-title":"Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part I, volume 254 of Lecture Notes of Computer Science","author":"Jensen","year":"1987"},{"key":"S0269888900007554_ref019","unstructured":"Craig I , 1991b, \u201cThe formal specification of ELEKTRA\u201d Technical report, Department of CS, University of Warwick."},{"volume-title":"Introduction to Expert Systems","year":"1990","author":"Jackson","key":"S0269888900007554_ref040"},{"key":"S0269888900007554_ref039","first-page":"233","volume-title":"Formal Specification of Computer Reasoning Systems","author":"Veld","year":"1994"},{"volume-title":"Applications of Formal Methods International Series in Computer Science","year":"1995","author":"Hinchey","key":"S0269888900007554_ref037"},{"key":"S0269888900007554_ref022","article-title":"Sinn und unsinn formaler spezificationssprachen fuer wissensbasierte systeme","author":"Fensel","year":"1994","journal-title":"Kuenstliche Intelligenz"},{"volume-title":"Proceedings of the IJCAI'91 Workshop on Software Engineering for Knowledge-Based Systems Sydney","year":"1991","author":"Jonker","key":"S0269888900007554_ref043"},{"key":"S0269888900007554_ref035","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012828"},{"volume-title":"Applications of Formal Methods","year":"1995","author":"Hoare","key":"S0269888900007554_ref038"},{"key":"S0269888900007554_ref034","first-page":"497","volume-title":"Handbook of Philosophical Logic, Vol. II. extensions of Classical Logic","author":"Hard","year":"1984"},{"volume-title":"Current Trends in Computer Science","year":"1993","author":"Gurevich","key":"S0269888900007554_ref032"},{"key":"S0269888900007554_ref084","first-page":"92","volume-title":"Readings in Knowledge Acquisition and Learning","author":"Buchanan","year":"1992"},{"key":"S0269888900007554_ref026","doi-asserted-by":"publisher","DOI":"10.1145\/48529.48530"},{"volume-title":"Applications of Formal Methods","year":"1995","author":"Peleska","key":"S0269888900007554_ref059"},{"key":"S0269888900007554_ref004","doi-asserted-by":"crossref","unstructured":"Anegle J. , Fensel D. , Landes D. and Studer R. , 1995, \u201cThe knowledge-based acquisition and representation language KARL\u201d (submitted for publication).","DOI":"10.1007\/978-1-4615-2275-1"},{"volume-title":"Proceedings of the 10th International Conference on Automated Deduction (CA DE'90), Volume 449 of Lecture Notes on Computer Science","year":"1990","author":"Heisel","key":"S0269888900007554_ref036"},{"volume-title":"Formal Specification of Complex Reasoning Systems","year":"1993","author":"Giunchiglia","key":"S0269888900007554_ref031"},{"volume-title":"9th Banff Knowledge Acquisition for KBS Workshop","year":"1994","author":"Fensel","key":"S0269888900007554_ref023"},{"key":"S0269888900007554_ref030","doi-asserted-by":"publisher","DOI":"10.1002\/int.4550100504"},{"volume-title":"Automated Generation of Model-Based Knowledge-Acquisition Tools","year":"1989","author":"Musen","key":"S0269888900007554_ref055"},{"key":"S0269888900007554_ref025","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900006767"},{"key":"S0269888900007554_ref024","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-2275-1"},{"key":"S0269888900007554_ref080","first-page":"356","volume-title":"Current Trends in Knowledge Acquisition","author":"Wetter","year":"1990"},{"key":"S0269888900007554_ref028","first-page":"52","volume-title":"Proceedings of Twelfth Symposium on Principles of Programming Languages","author":"Futatsugi","year":"1985"},{"key":"S0269888900007554_ref067","unstructured":"Todd B and Stamper R , 1993, The formal design and evaluation of a variety of medical diagnostic programs\u201d Technical Monograph PRG-109, Oxford University Computing Laboratory, 09."},{"volume-title":"Applications of Formal Methods","year":"1995","author":"Craigen","key":"S0269888900007554_ref020"},{"key":"S0269888900007554_ref082","unstructured":"Wielinga BJ and Breuker JA , 1986, \u201cModels of expertise\u201d In: Proceedings ECAI-86, pp 306\u2013318."},{"key":"S0269888900007554_ref029","unstructured":"Gebhardt F , 1995, \u201cMoMo: language and case studies\u201d Fabel-Report 36, GMC, Sankt Augustin, 07."},{"volume-title":"Rulebased Expert Systems: The Mycin Experiments of the Stanford Heuristic Programming Project","year":"1984","author":"Buchanan","key":"S0269888900007554_ref014"},{"key":"S0269888900007554_ref072","doi-asserted-by":"crossref","unstructured":"van Harmelen F , and Aben M , 1995, \u201cStructure preserving specification languages for knowledge-based systems\u201d International Journal of Human Computer Studies (formerly Journal of Man Machine Studies).","DOI":"10.1006\/ijhc.1996.0010"},{"volume-title":"Proceedings of the 5th International Conference on Software Engineering and Knowledge Engineering (SEKE'93)","year":"1993","author":"Voss","key":"S0269888900007554_ref079"},{"key":"S0269888900007554_ref027","doi-asserted-by":"publisher","DOI":"10.1016\/0933-3657(93)90015-U"},{"volume-title":"Formal Specification of Complex Reasoning Systems","year":"1993","author":"Treur","key":"S0269888900007554_ref069"},{"volume-title":"Validation, Verification and Test of Knowledge-Based System","year":"1991","author":"Ayel","key":"S0269888900007554_ref006"},{"key":"S0269888900007554_ref033","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"S0269888900007554_ref044","first-page":"501","volume-title":"Proceedings Expert Systems-91","author":"Karbach","year":"1991"},{"key":"S0269888900007554_ref073","article-title":"(ML)2: a formal language for KADS models of expertise","volume":"4","author":"van","year":"1992","journal-title":"Knowledge Acquisition"},{"key":"S0269888900007554_ref015","doi-asserted-by":"publisher","DOI":"10.1109\/MEX.1986.4306977"},{"key":"S0269888900007554_ref066","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/5.1.27"},{"volume-title":"Formal Specification of Complex Reasoning Systems","year":"1993","author":"Sierra","key":"S0269888900007554_ref063"},{"key":"S0269888900007554_ref049","unstructured":"Linster M , 1993, \u201cUsing the operational modeling language OMOS to represent KADS conceptual models\u201d Knowledge Acquisition."},{"key":"S0269888900007554_ref068","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58792-6_22"},{"key":"S0269888900007554_ref010","first-page":"105","volume-title":"Proceedings of the 2nd International Symposium of Formal Methods Europe (FME'94) volume 873 of Lecture Notes in Computer Science","author":"Bowen","year":"1994"},{"key":"S0269888900007554_ref060","unstructured":"Pierret-Goldbreich C and Talon X , 1995, \u201cAn algebraic specification of the dynamic behaviour of knowledge-based systems\u201d The Knowledge Engineering Review (submitted)."},{"key":"S0269888900007554_ref011","first-page":"47","volume-title":"KADS: A Principled Approach to Knowledge-Based System Development","author":"Breuker","year":"1993"},{"volume-title":"The Formal Specification of Advanced AI Architecture: Lecture Notes in Mathematics","year":"1991","author":"Craig","key":"S0269888900007554_ref018"},{"key":"S0269888900007554_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"S0269888900007554_ref008","first-page":"83","volume-title":"Proceedings Second KADS User Meeting","author":"Bauer","year":"1992"},{"volume-title":"Formal Specification of Complex Reasoning Systems","year":"1993","author":"Nakagawa","key":"S0269888900007554_ref056"},{"key":"S0269888900007554_ref013","unstructured":"Breuker JA , Wielinga BJ , van Someren M , de Hoog R , Schreiber ATh , de Greef P , Bredeweg B , Wielemaker J , Billault JP , Davoodi M and Hayward SA , 1987, \u201cModel Driven Knowledge Acquisition: Interpretation Models\u201d ESPRIT Project P1098 Deliverable Dl (task Al), University of Amsterdam and STL Ltd."},{"key":"S0269888900007554_ref001","unstructured":"Aben M. 1995, Formal methods in Knowledge Engineering PhD thesis, University of Amsterdam, Faculty of Psychology, 02."},{"key":"S0269888900007554_ref007","doi-asserted-by":"publisher","DOI":"10.1006\/knac.1993.1010"},{"volume-title":"Application of Formal Methods","year":"1995","author":"Anderson","key":"S0269888900007554_ref002"},{"volume-title":"Proceedings of the ECAI'94 Workshop on Formal Specification Methods for Knowledge-Based Systems","year":"1994","author":"Aronsson","key":"S0269888900007554_ref005"},{"volume-title":"Understanding Z: A Specification Language and its Formal Semantics volume 3 of Cambridge Tracts in Theoretical Computer Science","year":"1988","author":"Spivey","key":"S0269888900007554_ref064"},{"key":"S0269888900007554_ref061","unstructured":"Shadbolt N , Aitken S and Reichgelt LH , 1992, \u201cRepresenting kads models in QIL\u201d Working Paper WP006, Al Group, University of Nottingham."},{"volume-title":"The Common KADS Library for Expertise Modelling","year":"1994","author":"Breuker","key":"S0269888900007554_ref012"},{"key":"S0269888900007554_ref057","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(82)90012-1"},{"key":"S0269888900007554_ref016","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90016-5"},{"key":"S0269888900007554_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7"},{"volume-title":"The Z Notation: A Reference Manual","year":"1992","author":"Spivey","key":"S0269888900007554_ref065"},{"volume-title":"Materials KADS User Meeting, February 14\/15 1991","year":"1991","author":"Ueberreiter","key":"S0269888900007554_ref071"},{"key":"S0269888900007554_ref074","unstructured":"reprinted in KADS: A Principled Approach to Knowledge-Based System Development, 1993, Schreiber Ath , editors)."},{"key":"S0269888900007554_ref075","first-page":"272","volume-title":"Proceedings ECAI'92","author":"van Langevelde","year":"1992"},{"key":"S0269888900007554_ref076","unstructured":"van Melle W , 1979, \u201cA domain independent production rule system for consultation programs\u201d In: IJCAI-79 pp 923\u2013925."},{"key":"S0269888900007554_ref077","unstructured":"Velthuijsen H , 1992, \u201cThe nature and applicability of the blackboard architecture\u201d PhD thesis, University of Limburgh, Maastricht, The Netherlands."},{"key":"S0269888900007554_ref083","doi-asserted-by":"publisher","DOI":"10.1016\/1042-8143(92)90013-Q"},{"key":"S0269888900007554_ref085","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"S0269888900007554_ref086","doi-asserted-by":"publisher","DOI":"10.1109\/32.75412"},{"key":"S0269888900007554_ref041","first-page":"19","article-title":"Comparative evaluation of three expert system development tools: KEE, knowledge craft, ART","volume":"1","author":"Jaurent","year":"1986","journal-title":"Knowledge Engineering Review"},{"key":"S0269888900007554_ref052","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-7122-9"},{"key":"S0269888900007554_ref047","doi-asserted-by":"publisher","DOI":"10.1109\/64.215223"},{"volume-title":"AISB91, Artificial Intelligence and Simulation of Behavior","year":"1991","author":"Wetter","key":"S0269888900007554_ref081"},{"key":"S0269888900007554_ref078","first-page":"374","volume-title":"Proceedings of the European Simulation Multi-Conference (ESM'91)","author":"Velthuijsen","year":"1991"}],"container-title":["The Knowledge Engineering Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0269888900007554","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T14:42:46Z","timestamp":1767624166000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0269888900007554\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":86,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["S0269888900007554"],"URL":"https:\/\/doi.org\/10.1017\/s0269888900007554","relation":{},"ISSN":["0269-8889","1469-8005"],"issn-type":[{"type":"print","value":"0269-8889"},{"type":"electronic","value":"1469-8005"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}