Kontaktperson
Björn Bjurling
Senior Researcher
Kontakta BjörnAutomatiserad härledning
Automatiserad härledning är området som studerar algoritmer och mjukvara som möjliggör för datorer att föra logiska resonemang, för att utvinna ny kunskap från redan inhämtad kunskap. Nyttan med automatisk härledning är att vi kan formalisera komplexa avvägningar och bedömningar i tillämpade områden, så som till exempel medicinsk bedömning eller stadsplanering. Sådan formalisering ligger till grund för digitalisering.
Automatisk härledning är ett av de äldsta AI-områdena och har sina rötter i försöken att implementera generella problemlösare på 50-talet. Den fundamentala problemställningen i automatisk härledning är den att avgöra om ett påstående logiskt följer av en given mängd av påståenden. Problemställningen är generell och är central i flera industriella tillämpningar, såsom exempelvis schemaläggning, mjuk- och hårdvaruverifiering, logikprogrammering, AI och till och med i ekonomi.
Värde
För att beslutsprocesser och tillämpade resonemang ska kunna digitalisera behöver de först formaliseras (dvs översättas till ett språk som datorer kan förstå och effektivt hantera). Automatisk härledning bidrar till sådan formalisering på tre sätt: dels genom att uttrycka domänspecifik kunskap och tillämpade resonemang i existerande logiska system, dels genom att anpassa existerande logiska system eller utveckla nya logiska system som passar till den aktuella tillämpningen, och dels genom att implementera/automatisera det formaliserade resonemanget på ett effektivt sätt.
Utmaningar
Den främsta utmaningen i att formalisera tillämpade resonemang är att de ofta bygger på heuristik, erfarenhet och så kallat common-sense resonemang. Många existerande och välkända effektiva system (tex matematiska metoder) lämpar sig sällan för sådana tillämpningar och resulterar därför i ineffektiva lösningar. Med metoder från automatisk härledning kan vi hitta anpassade avvägningar mellan effektiv beräkning och tillräcklig uttryckskraft i formaliseringen av problemet.
Ebjudande och löfte
RISE har lång erfarenhet av tätt samarbete med kunden för att förstå och kunna att formalisera kundens specifika industriella problem. Tillsammans med kunden tar vi fram realistiska målsättningar och kvalitetskrav på slutprodukten. Projekt där metoder från automatisk härledning mynnar som regel ut i algoritmer och proof-of-concept-implementationer av mjukvaruuverktyg.