CS 2800: Logic and Computation Lente 2019

Deze cursus biedt een inleiding tot de formele logica en de diepgaande verbanden met informatica. Logica wordt gepresenteerd vanuit een rekenkundig perspectief met behulp van het ACL2 Sedantheorem proving systeem. Het doel van de cursus is om fundamentele methodes te introduceren voor het modelleren, ontwerpen en beredeneren van berekeningen, inclusief propositionele logica, recursie, inductie, redeneren op basis van vergelijking, beëindigingsanalyse, herschrijven en verschillende bewijstechnieken. We laten zien hoe we logica kunnen gebruiken om de syntax en semantiek van de ACL2s taal te formaliseren, een eenvoudige op LISP gebaseerde taal met contracten. Vervolgens gebruiken we de ACL2s taal om formeel te redeneren over programma’s, om systemen op verschillende abstractieniveaus te modelleren, om interfaces tussen systemen te ontwerpen en te specificeren en om over dergelijke samengestelde systemen te redeneren. We onderzoeken ook beslissingsprocedures voor fragmenten van de logica van de eerste orde en hoe dergelijke beslissingsprocedures kunnen worden gebruikt om modellen van systemen te analyseren.

De vereisten zijn een basiskennis van functioneel programmeren (CS 2500) en discrete structuren (CS 1800). Als u niet beschikt over deze achtergrond, moet u de toestemming van uwinstructeur.

Studenten die het college zijn verplicht om Piazza check voor aankondigingen dagelijks.