澳大利亚西悉尼大学张焰教授学术讲座通知
时间:2015-01-09


澳大利亚西悉尼大学张焰教授学术讲座通知

    应计算机学院智能与分布计算实验室邀请,澳大利亚西悉尼大学张焰教授将于2015年1月16日(周五)下午来计算机学院举行专题讲座,欢迎广大师生参加。

    讲座题目:Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness

    讲座时间:2015年1月16日(周五)下午2:30开始
    讲座地点:计算机学院会议室(南1楼433室)


讲座题目:Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness

Yan Zhang
Artificial Intelligence research Group
School of Computing, Engineering and Mathematics
University of Western Sydney
 
讲座摘要:
Logic programs with ordered disjunction (LPODs) (Brewka 2002) generalize normal logic programs by combining alternative and ranked options in the heads of rules. It has been showed that LPODs are useful in a number of areas including  game theory, policy languages, planning and argumentations. In this paper, we extend propositional LPODs to the first-order case, where a classical second-order formula is defined to capture the stable model semantics of the underlying first-order LPODs. We then develop a progression semantics that is equivalent to the stable model semantics but naturally represents the reasoning procedure of LPODs. We show that on finite structures, every LPOD can be translated to a first-order sentence, which provides a basis for computing stable models of LPODs. We further study the complexity and expressiveness of LPODs and prove that almost positive LPODs precisely capture first-order normal logic programs, which indicates that ordered disjunction itself and constraints are sufficient to represent negation as failure.

讲者简介:
Yan Zhang is a professor in University of Western Sydney, where he leads the university research group on Artificial Intelligence. Yan's research interests include knowledge representation and reasoning, model checking and update, and information security. In recent years he has been focusing his study on logic foundations of first-order answer set programming. Yan and his colleagues and students have published a number of high standard publications on this topic, and developed two first-order ASP solvers.

http://www.scm.uws.edu.au/~yan/