Logic based problem solving: from theory to practice

Title: Logic based problem solving: from theory to practice
Speaker: Dr. Yi Zhou (University of Western Sydney, Australia)
Time: 15:00, Wednesday, June 27th, 2012
Venue: Lecture Room, 3rd Floor, Building 5#, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Outline:

1. Logic based problem solving

1.1. solving problems without algorithms

1.2. Logic formalisms (including SAT, SMT, FOL, Prolog, Datalog and so on)

1.3. Logic based problem solving: the state of art (how successful the logic based approaches are)

1.4. Declarative programming vs imperative programming

2. Answer set programming

2.1. Answer set programming: a new foundation

2.2. Relationships to other logic formalisms (what are the relationships between ASP and SAT, SMT, etc.)

2.3. A new direction for ASP solving (and its preliminary implementation)

2.4. Disjunctive ASP and P vs NP

3. Open topics and problems (some open research topics and problems, which have the potential to be high-level work, e.g. AIJ level topics)

Abstract:
Logic based problem solving approaches, such as propositional satisfiability problem, relational calculus, Satisfiability Modulo Theories, prolog, Datalog, circumscription and default logic, are one of the central topics in computer science, and have profound applications to many related areas, e.g., software engineering, artificial intelligence, database, WWW, information security, bioinformatics and so on. More importantly, in the last decade, significant progresses have been made to implement these logical formalisms for solving real world problems.

This talk is about Answer Set Programming, a traditional yet modern logic based declarative programming paradigm, which has its root deeply planted in the above logic approaches but with new and promising features. We reconstruct the foundation of Answer Set Programming, and show that it is deeply related to all the above logic approaches. Based on these theoretical results, we present a new direction of answer set solving, whose promising future is evidenced by a first implementation. We also discuss some deep relationships between Answer Set Programming and computational complexity, e.g. the P vs NP problem.

Short bio:
Dr. Yi Zhou is now a lecturer at the Artificial Intelligence Research Group in University of Western Sydney. His research focuses on logic foundations in computer science and artificial intelligence, and their applications to other areas in computer science, e.g., model checking and verification, AI planning, information security, WWW and so on. His recent publications include 4 articles in the predominant AI journal – Artificial Intelligence. More details can be found in his website: https://staff.scm.uws.edu.au/~yzhou/