|  |
02286 Logic in computer science, artificial intelligence and multi-agent systems |
| | |  | Danish title:
| Logik i datalogi, kunstig intelligens og multiagent-systemer | Language:
| | Point
(ECTS )
| 7.5 | Course type:
|
| | |
| Schedule:
| E1A
| Scope and form: | Lectures, exercises and mandatory assignments or project. | Duration of Course:
| 13 weeks | Date of examination:
| E1A,
F1A
| Type of assessment:
| | Exam duration:
| | Aid:
| | Evaluation: | | Qualified Prerequisites: | , | Optional Prerequisites: | , |
| General course objectives:
| To provide the student with knowledge and understanding of a variety of logical approaches, methods, and techniques used for specification, modelling, and formal reasoning in computer science, artificial intelligence and multi-agent systems.
|
| Learning objectives: | | A student who has met the objectives of the course will be able to: | - explain the underlying ideas and principles of logical specification and reasoning in CS (computer science), AI (artificial intelligence) and MAS (multi-agent systems)
- use classical logic for knowledge representation, problem formalization, and reasoning in computer science and AI
- explain the concept of logical deductive system, and the importance of soundness, completeness, and decidability of a deductive system
- explain and apply the systems of semantic tableau and natural deduction in classical logic to logical deduction and reasoning
- explain and apply the method of first-order resolution for automated deduction
- explain the logical problems of model checking and satisfiability testing in the context of reasoning in CS and AI
- describe the variety of modal and temporal logics used in CS, AI and MAS and explain the basics of Kripke semantics
- choose and apply suitable modal logical languages for knowledge representation, problem analysis, and logical reasoning in various areas of CS and AI, incl. temporal and epistemic reasoning
- describe and apply various logical systems for formalization of, and reasoning about, individual and collective knowledge and strategic abilities in multi-agent systems
- explain and apply the method of semantic tableaux for testing satisfiability and logical deduction in modal, temporal, and epistemic logics
- independently explore and assess the relevant literature
| Content:
| Overview on classical (propositional and first-order) logic as a language for problem formalization and framework for reasoning in CS and AI using classical deductive systems: natural deduction, semantic tableau, and resolution. Automated reasoning and applications to CS and AI. Modal, temporal, and epistemic logics for specification and reasoning in CS and AI. Logics for specification and reasoning in multi-agent systems: logics of knowledge, beliefs, actions and strategic abilities of agents and coalitions. The method of semantic tableaux for testing satisfiability and logical deduction in modal, temporal, and epistemic logics.
|
| Course literature:
| A combination of lecture notes and other selected reading materials will be provided during the course.
|
| Responsible:
| , 322, 024, (+45) 4525 3376,
| Department:
| 02 Department of Informatics and Mathematical Modeling | Registration Sign up:
| At CampusNet |
|
|
| | Last updated:
April 25, 2012 |
See course in DTU Course base
|