Een essentieel kenmerk van intelligente systemen is de manipulatie van aanwezige kennis teneinde "nieuwe" kennis af te leiden. Veel van deze technieken zijn samen te vatten onder de noemer automatisch redeneren. In het college wordt achtereenvolgens behandeld: geschiedenis, taxonomie en toepassingen AR, eenvoudige stellingenbewijzers op basis van semantische bomen, het resolutieprincipe, Davis-Putnam procedure, 1e-orde stellingenbewijzers, effect van het toevoegen van functiesymbolen en gelijkheid, hyperresolutie, UR-resolutie, paramodulatie, Otter, het testen op vervulbaarheid met behulp van stochastische algoritmen, argumentatie, abductie, het genereren van nieuwe regels met inductie, reinforcement leren van nieuwe regels, holistische vormen van redeneren zoals bijvoorbeeld Thagard's coherentietheorie. In een begeleidend practicum wordt je gevraagd een stellingenbewijzer te implementeren in een programmeertaal naar keuze.

http://www.cs.uu.nl/education/vak.php?vak=INFOAR&jaar=2008