Het wetenschappelijk onderzoeksdomein Kennisrepresentatie en redeneren ( KRR) beoogt het ontwikkelen van formele talen (logica's) die geschikt zi jn om kennis uit te drukken en van inferentiemethodes om te redeneren ov er kennis uitgedrukt in die talen. Een van de hoofddoelen van KRR is het bouwen van een kennisbanksysteem (KBS): een systeem waarin een menselij ke expert zijn kennis over een bepaald domein opslaat en waarmee verschi llende taken in dat domein opgelost worden door het toepassen van infere ntiemethodes. In deze thesis stellen we een uitbreiding van klassieke lo gica voor als geschikte logica voor een KBS en onderzoeken we verschille nde vormen van inferentie. De eerste vorm van inferentie die we onderzoeken is propagatie: uit een logische theorie feiten afleiden die zeker waar zijn in elk model van de theorie. We onderzoeken voornamelijk een benaderende maar efficiënte vo rm van propagatie, die bovendien op een symbolische manier uitgevoerd ka n worden. We beschrijven verschillende toepassingen van propagatie. De tweede vorm van inferentie is propositionalisatie: het omzetten van e en logische theorie die variabelen mag bevatten naar een equivalente pro positionele theorie. Propositionalisatie wordt vaak gebruikt als eerste stap in systemen voor eindige model generatie. Eindige model generatie v ormt op zich ook een belangrijke vorm van inferentie. We tonen aan hoe p ropositionalisatie verbeterd kan worden door overtollige informatie toe te voegen aan een theorie. Deze overtollige informatie kan berekend word en met behulp van symbolische propagatie. Ten derde bestuderen we hoe fouten in een logische theorie opgespoord ku nnen worden. De methode die we voorstellen bestaat uit het interactief o verlopen van formele bewijzen van de inconsistentie van een theorie. We tonen dat model generatoren die gebaseerd zijn op propagatie gebruikt ku nnen worden om automatisch zulke formele bewijzen op te stellen. Tenslotte bestuderen we model revisie: het aanpassen van een model van e en theorie wanneer nieuwe vereisten gesteld worden. Model revisie heeft onder andere toepassingen in herconfiguratie en herplanningsproblemen. W e laten zien hoe model revisie problemen aangepakt kunnen worden door he t oplossen van opeenvolgende model generatie problemen.
展开▼
