Ræsonnering er evnen til at drage logiske slutninger. Formålet med kurset er at give de studerende en introduktion til automatiske og interaktive computersystemer til ræsonnering om matematiske teoremer samt egenskaber ved it-systemer. Det vil dække teoretisk indsigt samt praktiske færdigheder i relevante bevisassistenter. En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:

• forklare de grundlæggende begreber introduceret i kurset
• udtrykke matematiske teoremer og egenskaber ved it-systemer formelt
• mestre bevissystemet naturlig deduktion
• relatere førsteordenslogik, højereordenslogik og typeteori
• konstruere formelle beviser i procedural stil og i deklarativ stil
• bruge automatiske og interaktive computersystemer til automatiseret ræsonnering
• evaluere troværdigheden af bevisassistenter og relaterede værktøjer
• kommunikere løsninger på problemer på en klar og præcis måde

Bevissystemet naturlig deduktion, førsteordenslogik, højereordenslogik og typeteori. Formelle beviser i procedural stil og i deklarativ stil ved hjælp af automatiske og interaktive bevisførere. Bevisassistenten Isabelle i kunstig intelligens og datalogi. 17. april, 2020