| vorm | groep | tijd | week | zaal | docent | |
|---|---|---|---|---|---|---|
| college | di 13.15-15.00 | 46-50 | BBL-079 | Gerard Vreeswijk |
|
|
| 2-4 | BBL-079 | |||||
| do 9.00-10.45 | 46-51 | BBL-083 | ||||
| 2-4 | BBL-083 | |||||
| practicum | groep 1 | di 14.00-15.00 | 46-50 | BBL-115 CLZ | Gerard Vreeswijk Bas van Gijzel Antonios Thomas |
|
| 2-4 | BBL-115 CLZ | |||||
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.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.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.