Content, progress and pedagogy of the module

Disclaimer
This is an English translation of the module. In case of discrepancy between the translation and the Danish version, the Danish version of the module is valid.

PURPOSE 
hat the student acquires knowledge and skills about the use of logic to formalize and solve computational problems

JUSTIFICATION
Logical languages ​​and inference techniques provide powerful tools for solving complex problems in areas such as artificial intelligence and program analysis. The course will enable students to understand and use logic-based technology

Learning objectives

Knowledge

The course introduces syntax, semantics, inference techniques, and applications of important types of logic. Specific topics covered in the course may include: 

Syntax, semantics and applications of various logics, such as 

• Statement logic 
• Extensions of Statement Logic, such as quantified Boolean formulas and satisfiability modulo theories. 
• First-order predicate logic, Higher-order predicate logic, Modal logic. 
• Horn clause logic for logic programming 
• Hoare logic for program analysis

Data structures and techniques for logical inference:  

• Advanced methods and data structures for solving satisfiability (eg DPLL,CDCL,BDDs). 
• Automated proof techniques 

Applications:

• Knowledge representation and reasoning in artificial intelligence 
• Planning 
• Analysis of software

Skills

• explain key theoretical and practical aspects of logics introduced in the course 
• use correct subject terminology and notation

Competences

• could identify appropriate logics for formalizing and solving specific problems
• be able to identify and use suitable algorithms and software tools for solving a problem in computational logic

Type of instruction

Extent and expected workload

The student is expected to spend 30 hours per ECTS, which for this activity means 150 hours.

Exam

Exams

Additional information