Automatisch redeneren

Website:website met extra informatie
Vakcode:INFOAR
Studiepunten:7.5 ECTS
Periode:periode 2 (week 46 t/m 5, dwz 15-11-2010 t/m 4-2-2011; herkansing week 11)
Timeslot:C
Deelnemers:tot nu toe 40 inschrijvingen
Rooster:Let op: m.i.v. het collegejaar 2008/2009 is het rooster te vinden in Osiris
Docenten:Dit is een oud rooster!
vormgroeptijdweekzaaldocent
college          Gerard Vreeswijk
 
practicum groep 1        Gerard Vreeswijk
Bas van Gijzel
Antonios Thomas
   
Inhoud: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 Java.
Literatuur:Gerard Vreeswijk, Automatisch Redeneren, collegedictaat versie 2009/2010. Te koop aan de balie.
Werkvorm:Per week 2 keer 1 uur hoorcollege direct gevolgd door 1 uur practicum (dinsdag) of 1 uur werkcollege (donderdag).
Toetsvorm:Het vak wordt beoordeeld aan de hand van twee toetsen (T1,T2) en twee practicumopdrachten (P1, P2). Het toetscijfer is gelijk aan het gemiddelde van de toetsen. Het practicumcijfer is gelijk aan het gemiddelde van de practicumresultaten. Er zijn inleveropgaven. Deze kunnen theoretisch of praktisch van aard zijn. Met zes als tenminste voldoende beoordeelde inleveropgaven kan een theoretische toets met een punt worden gecompenseerd. Met minder voldoendes geldt een proportionele verhoging. (Bv. drie voldoendes is goed voor een half punt compensatie op één theoretisch onderdeel.) Het eindcijfer bedraagt round(0.5*T+0.5*P). Afronding gebeurt op halven boven de zes en op helen onder de zes. Als een van de drie cijfers P1, P2, T ontbreekt, blijft het vak onvoltooid. Bij het tentamen mag een dubbelzijdig A4-aantekeningenblaadje worden gebruikt, maar geen literatuur.
Inspanningsverplichting voor aanvullende toets:Om aan de aanvullende toets te mogen meedoen moet de oorspronkelijke uitslag minstens 4 zijn.
Beschrijving:Een selectie van vaardigheden die in de loop van de cursus kunnen worden getoetst:

Het kunnen bewijzen van een propositioneel geldige sequent met behulp van de klassieke tableaumethode. Uit het hoofd kennen van regels van KE en SAKE, het kunnen bewijzen van een propositioneel geldige sequent met KE en SAKE, kunnen beargumenteren van soundness en volledigheid van klassieke tableaumethoden en KE (niet van SAKE), redelijk beoordelingsvermogen hebben over mogelijkheden en onmogelijkheden van propositionele stellingenbewijzers, bewijzen van een geldige sequent in 1e-orde calculus met klassieke tableaumethode, met vrije-variabele tableaumethode, kunnen aangeven welke 1e-orde termen unificeren en welke niet, zinnige kanttekeningen kunnen plaatsen bij bewijs van correctheid / volledigheid unificatiealgoritme, kunnen bewijzen van een geldige sequent in 1e-orde calculus met gelijkheid met klassieke tableaumethode, kunnen bewijzen van een geldige sequent in 1e-orde calculus met gelijkheid met vrije-variabele tableaumethode, iets kunnen zeggen over heuristieken die worden toegepast bij laatstgenoemde bewijsmethode, verschillende manieren voor CNF/DNF/3CNF-conversie kunnen noemen en demonstreren, weten elke conversie niet equivalentie-behoudend zijn, technieken beheersen om propositionele en 1e-orde clause sets op te schonen, DPPL, DPP kunnen toepassen, zinnige kanttekeningen kunnen plaatsen bij volledigheidsbewijs binaire resolutie, weten wat hyperresolutie is en waarvoor het gebruikt wordt, verschil kunnen aangeven tussen branche-merge en DPLL, fragmenten van 1e-orde resolutie kunnen geven, termen kunnen demoduleren, eenvoudige paramodulatie kunnen toepassen, algoritme GSAT kunnen reproduceren, penalty-functie GSAT kunnen geven, geldigheid van geldige epsilon-afleidingen kunnen bewijzen, ongeldigheid van ongeldige epsilon-afleidingen kunnen bewijzen met behulp van tegenvoorbeelden, verschil locaal/globaal argumenteren kunnen aangeven, via regressie sterkste argument kunnen vinden, support kunnen uitrekenen van proposities, stabiele verzamelingen van gerichte argumentgraaf kunnen geven, statustoekenning aan argumenten in gerichte argumentgraaf kunnen geven, discrete en reeelwaardige coherentienetwerken kunnen beschrijven. Uit een enkele regels, data en tegenstellingen met coherentieprincipes een coherentienetwerk kunnen opstellen, absolute en relatieve maat voor globale coherentie kunnen geven, zinnige kanttekeningen kunnen plaatsen bij connectionistische versie van harmonisatiealgoritme.
wijzigen?