可计算性逻辑课程 (Lecture Course on Computability Logic)

Computability Logic

可计算性逻辑

Graduate course taught at the Institute of Artificial Intelligence of Xiamen University in June-July 2007 by

Giorgi Japaridze

• The professor 教授
• Briefly about computability logic 可计算性逻辑简介
• Literature 文 徍�
• Syllabus 教学大纲
• Lecture notes 讲稿
• Homework assignments 课外作业

---

The professor

教授

Giorgi Japaridze was born in Georgia, former Soviet Union. He received two PhDs, one from Moscow State University (in logic) and the other from the University of Pennsylvania (in computer science). Currently he works in the Computer Science Department of Villanova University, USA. The primary area of his research interests is logic and its applications in computer science. Computability logic - the subject of the present course - is an approach recently introduced by him.

乔治.札帕日泽?生于前苏联格鲁吉亚共和国?拥有两个博士学位?莫斯科大学的?逻辑学?和 宾夕法尼亚大学的?计算机科学?。徍驹谑敲拦�维拉诺瓦大学计算机科学系的教授。主要研究领域?逻辑学以及逻辑学在计算机科学中的应用。可计算性逻辑 ?这次课程的题目?-- 是他近年提出来的。这是第一次对中国进行学术访问.

• 办公室: 科研楼?2?XXXX
• 办公时间: 上课前后一个小时?或者预约.
• Email: giorgi.japaridze@villanova.edu
• 电话: 258XXXX
• 个人网页: http://www.csc.villanova.edu/~japaridz/
• 最近的照片
• 在因特网上找他

---

Briefly about computability logic

Computability is certainly one of the most interesting and fundamental concepts in mathematics, philosophy and computer science, and it would be more than natural to ask what logic it induces. Let us face it: this question has not only never been answered, but never even been asked within a reasonably coherent and comprehensive formal framework. This is where Computability Logic (CL) comes in. It is a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader and more proper sense, computability logic is not just a particular theory but an ambitious and challenging program for redeveloping logic following the scheme "from truth to computability". It was introduced by Japaridze in 2003 and, at present, still remains in its infancy stage, with open problems prevailing over answered questions. It is largely a virgin soil offering plenty of research opportunities, with good chances of interesting findings, for those with interests in logic and its applications in computer science, including theory of computation and artificial intelligence.

Computation and computational problems in CL are understood in their most general, interactive sense, and are precisely seen as games played by a machine (computer, agent, robot) against its environment (user, nature, or the devil himself). Computability of such problems means existence of a machine that always wins the game. Logical operators stand for operations on computational problems, and validity of a logical formula means being a scheme of "always computable" problems.

Remarkably, classical, intuitionistic and linear (in a broad sense) logics turn out to be three natural fragments of CL. This is no accident. The classical concept of truth is nothing but a special case of computability -- computability restricted to problems of zero interactivity degree. Correspondingly, classical logic is nothing but a special fragment of CL. One of the main -- so far rather abstract -- intuitions associated with intuitionistic logic is that it must be a logic of problems (Kolmogorov 1932); this is exactly what CL is, only in a much more expressive language than intuitionistic logic. And one of the main -- again, so far rather abstract -- claims of linear logic is that it is a logic of resources. Reversing of the roles of the machine and its environment turns computational problems into computational resources, which makes CL a logic of resources, only, again, in a more expressive language than that of linear logic, and based on an intuitively convincing and mathematically strict resource semantics rather than some naive philosophy and unreliable syntactic arguments. For more about CL vs. linear logic, visit Game Semantics or Linear Logic?.

The CL paradigm is not only about "what can be computed", but equally about "how can be computed". This opens potential application areas far beyond pure computation theory, such as:

• Knowledgebase systems. CL is an appealing alternative to the traditional knowledge base, knowledge representation and query logics. Its advantages include:
  • CL is a logic of interaction, and this is what a good knowledgebase logic needs to be. After all, most of the real knowledgebase and information systems are interactive.
  • CL is resource-conscious: the potential knowledge provided by a disposable pregnancy test device is knowledge of only one (even though an arbitrary one) woman's pregnancy status, but not two. CL naturally captures this sort of extremely relevant differences while the traditional systems fail to account for them.
  • CL naturally differentiates between truth and an agent's actual ability to find/compute/tell what is true. To achieve similar effects, traditional knowledgebase logics have to appeal to the controversial, messy and troublemaking epistemic constructs.
• Systems for planning and action. CL might be a reasonable alternative to the traditional AI planning logics. Its advantages include:
  • CL is a logic of interaction, and planning systems should be well able to account for an agent's interaction with the environment.
  • A good planning logic should be able to naturally account for the fact that with one ballistic missile one can destroy only one (even though an arbitrary one) target but not two. The resource-conscious CL fits the bill.
  • CL is a logic of knowledge and informational resources, which automatically takes care of the knowledge preconditions problem.
  • CL-based planning systems appear to be immune to the notorious frame problem.
• Constructive applied theories. CL is a conservative extension of classical logic, which makes it a reasonable alternative to the latter in its most traditional and unchallenged application areas. In particular, it makes perfect sense to base applied theories (such as, say, Peano arithmetic) on CL instead of classical logic. The advantages of doing so include that CL-based applied theories, compared with their classical-logic-based counterparts, are:
  • Expressive: the language of classical logic is only a modest fraction of the language of CL.
  • Computationally meaningful: every theorem of a CL-based theory represents a computable problem rather than just a true statement.
  • Constructive: any proof of a formula F in a CL-based theory effectively encodes a solution to the computational problem represented by F.

The primary online source of on the subject is maintained at the Computability Logic Homepage.

可计算性逻辑简介

可计算性无疑是数学、哲学和计算机科学中最有趣的、基本的概念之一。人们自然会问它推导出来的是什么逻辑?可事实上这个问题不仅从未得到过回答?甚至在徍�关的广泛领域里从来还没有 被提及过?这正是可计算性逻辑的起源。它是可计算性的形式理论?正如经典逻辑是真理的形式理论。更确切的说?可计算性逻辑不是一种特定的理论?而是一个充满雄心和挑战的计划 ?为在^从真理到可计算性 ?框架下重振逻辑。可计算性逻辑是Japaridze在2003年提出来的?目前还处于初级阶段?需解决的问题超过已解决的问题。这是一片还未开垦的领域?为那些对逻辑和逻辑在计算机方面的应用?以及对计算人工智能理论感兴趣的人们提供了很多研究和有趣发徍镜暮没�会。

计算和可计算问题在可计算性逻辑中被最普遍地理解为交互的? 它们被当作一种博弈。博弈的一方是机器?计算机、智能体、机器人??另一方是环境?用户、自然、或者魔鬼本身 ??问题的可计算性意味着存在一个机器总能赢得这个博弈?逻辑运算表示在可计算问题上的操作?一个逻辑公式的有效性表示它存在^总是可计算的 ?问题。

值得一提的是?经典的、直觉的和?性的?广义上?逻辑成为可计算性逻辑的三部分。真理的经典概念只是可计算性的特例----零交互问题的可计算性?徍�应的?经典逻辑只是可计算 性逻辑的特殊部分。和直觉逻辑徍�关联的?至今颇抽徎业�?主义是它应该是一种问题的逻辑?这也就是可计算性逻辑?只不过采用了比直觉逻辑更富表达能力的构造语言。 ?性逻辑最重要的?又一颇抽徎业�?声称是它是一种资源逻辑?把机器和环境的角色换一下?计算问题就变成计算资源?这使得可计算性逻辑成为资源逻辑?同样也只是采用了比?性逻辑更富表达能力的构造语 言?并且是基于令人信服的直觉和严格数学语义,而非一些幼稚的哲学和不可信的依据句法构造推论的资源语义。要更徎合傅亓私饪杉扑阈月呒�和?性逻辑的比较?可以访问网站博弈语义还是?性逻辑 ?

可计算性逻辑的实例不仅是关于^什么是能计算的 ??徍�同程度的也关于^如何被计算 ?。这开放了远不止单纯计算理论的潜在应用领域?比如?

l 知识库系统 可计算性逻辑对于传统的知识库?知识表示和查询逻辑是个有吸引力的选择?它的优势包括?

Ø 可计算性逻辑是交互的?这是好的知识库逻辑需要具备的?毕竟徍臼抵卸嗍�的知识库和信息系统是交互的。

Ø可计算性逻辑是有资源意识的?一次性的验孕设备提供的潜在信息只是一个?即使任意一个?妇女的怀孕情况?而不是两个。可计算性逻辑自然地捕捉到了这种极微小的区别?但传统的系统无法说明这些。

Ø可计算性逻辑很容易区分真理和一个主体发徍�/计算/认知什么是正确的实际能力。为达到徍�似的效果?传统的知识库逻辑必须借助有争议的、混乱的和惹麻烦的认知构造。

l 规划和行为系统 可计算性逻辑可能是传统人工智能规划逻辑的合理替代? 它的优点如下?

Ø可计算性逻辑是交互的?规划系统应该能很好的解决一个主体和环境的交互。

Ø一个良好的规划逻辑应该能够容易的说明这样的情况?即同一个弹道导弹可摧毁只有一个(即使任意一)目标,而不是两个?有资源意识的可计算性逻辑正好符合要求。

Ø可计算性逻辑是知识和信息资源的逻辑?它能自动地处理知识前条件(knowledge preconditions)问题。

Ø基于可计算性逻辑的规划系统似乎能避免臭名昭著的框架(frame)问题。

l 构造的应用理论 可计算性逻辑是经典逻辑的保守扩展?这使得可计算性逻辑在多数传统和没挑战性的应用领域里取代经典逻辑?尤其是很值得让可计算性逻辑代替经典逻辑作为应用理论?比如皮埃诺算术?的基础。这么做的好处包括基于可计算性逻辑的应用理论 比较基于经典逻辑的徍�应部分有下面的优点?

Ø富有表达力?经典逻辑的语言只是可计算性逻辑语言的一小部分。

Ø可计算的意义?基于可计算性逻辑的理论代表了可计算的问题而不仅是真语句。

Ø 建设性的?基于可计算性逻辑理论中的公式F的任何证据都可以有效地编码成由F代表的可计算问题的解答。

最主要的可计算性逻辑的网页

---

Literature

文徍�

Selected papers on computability logic

关于可计算性逻辑选择的论文

The official journal versions of the following papers may be slightly different from the corresponding online preprints. It is recommended that you try to use the journal version first. Access to some journals may be restricted though, in which case you may download the online preprint.

以下论文在官方杂志上的版本可能跟网上的preprint稍微有一点不同。建议先尝试使用官方的杂志?除非它不能打开?再用preprint。

1. G.Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pp.1-99. [SCI,AMS]
   Official journal version Online preprint Erratum
2. G.Japaridze, Propositional computability logic I. ACM Transactions on Computational Logic 7 (2006), No. 2, pp. 302-330. [SCI,AMS]
   Official journal version Online preprint
3. G.Japaridze, Propositional computability logic II. ACM Transactions on Computational Logic 7 (2006), No. 2, pp. 331-362. [SCI,AMS]
   Official journal version Online preprint
4. G.Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), No.4, pp. 489-532. [SCI,AMS]
   Official journal version Online preprint
5. G.Japaridze, Computability logic: a formal theory of interaction. In: Interactive Computation: The New Paradigm. D.Goldin, S.Smolka and P.Wegner, eds. Springer Verlag, Berlin 2006, pp. 183-223. [AMS]
   Official book version Online preprint
6. G.Japaridze, From truth to computability I. Theoretical Computer Science 357 (2006), pp. 100-135. [SCI,AMS]
   Official journal version Online preprint
7. G.Japaridze, From truth to computability II. Theoretical Computer Science 379 (2007), pp. 20-52. [SCI,AMS]
   Official journal version Online preprint
8. G.Japaridze, Intuitionistic computability logic. Acta Cybernetica 18 (2007), No.1, pp. 77-113. [AMS]
   Official journal version Online preprint
9. G.Japaridze, The logic of interactive Turing reduction. Journal of Symbolic Logic 72 (2007), No.1, pp. 243-276. [SCI,AMS]
   Official journal version Online preprint
10. G.Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), No.3, pp. 187-227. [SCI,AMS]
    Official journal version Online preprint
11. G.Japaridze, In the beginning was game semantics. In: Games: Unifying Logic, Language and Philosophy . O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp. 249-350. [AMS]
    Official book version Online preprint
12. G.Japaridze, Many concepts and two logics of algorithmic reduction. Studia Logica 91 (2009), No.1, pp. 1-24. [AMS]
    Official journal version Online preprint

Precursors of computability logic (most relevant pre-2003 papers)

可计算性逻辑的^先驱 ? ?2003年以前最有关系的论文?

1. A series of papers on game semantics by Lorenzen and his student Lorenz, written at the end of the 1950s and during the 1960s.
2. A series of papers on game semantics by Hintikka and his school, beginning from the 19960s.
3. A.Blass, Degrees of indeterminacy of games. Fundamenta Mathematicae 77 (1972), pp. 151-166.
4. J.Y.Girard, Linear logic. Theoretical computer science 50 (1887), pp. 1-102.
5. A.Blass, A game semantics for linear logic. Annals of Pure and Applied Logic 56 (1992), pp. 183-220.
6. G.Japaridze, A constructive game semantics for the language of linear logic. Annals of Pure and Applied Logic 85 (1997), No.2, pp.87-156.
7. G.Japaridze, The logic of tasks . Annals of Pure and Applied Logic 117 (2002), pp.263-295.
   

Some related papers by Chinese authors

一些中国作者的有关论文

The following papers are primarily or partially devoted to the logic of tasks (任务逻辑), introduced in item [7] (2002) of the previous list. The logic of tasks is essentially nothing but a special, relatively simple fragment of computability logic in a somewhat naive form. The author treats it as an "experimental stage" on the way leading to developing computability logic. The latter is a generalization and substantial refinement of the former, but otherwise the two are fully consistent, and results concerning the logic of tasks would typically automatically extend to computability logic as well.

• 王国俊 许文艳 从事实逻辑到任务逻辑 模糊系统与数学 2004年 18卷 1期 起止页码?1-8.
  Guojun Wang and Wenyan Xu,F rom the logic of facts to the logic of tasks. Fuzzy Sy stems and Mathematics18?2004), No.1, pp.1-8.
• 许文艳 荆云鹏 任务逻辑中的定理 模糊系统与数学 2006年 20卷 6期 起止页码?15-20.
  Wenyan Xu and Yunpeng Jing, Theorems in the logic of tasks . Fuzzy Sy stems and Mathematics20 (2006), No.6, pp.15-20.
• 张会 李思昆 描述任务逻辑及其应用 计算机学报 2006年 29卷 3期 起止页码?488-494.
  Hui Zhang and Sikun Li,The description logic of tasks: from theory to practice. Chinese Journal of Computers29 (2006), No.3, pp.488-494.
• 张会 李思昆 面?交互的主体能力描述和推理方法研究 计算机研究与发展 2006年 43卷 8期 起止页码?1439-1444.
  Hui Zhang and Sikun Li,Interaction-oriented ability specification and reasoning. Journal of Computer Research and Development 43 (2006), No.8, pp.1439-1444.
• 张会 李思昆 吴鹏 虚拟实体组织行为建模方法研究 系统仿真学报 2006年 18卷 1期 起止页码: 252-254.
  Hui Zhang, Sikun Li and Peng Wu, Behavior Represention and Modelling of Organizational Virtual Entities. Journal of System Simulation 18 (2006), No.1, pp.252-254.

---

Syllabus

教学大纲

Meeting times: Tuesdays and Thursdays 4:30-6:10.
授课时间?星期二和星期四 4:30-6:10.

课室 (Classroom): 教学楼 202

There is no textbook for this course. All written materials that you may need (including lecture notes) will be made available through this web site.
这门课程没有课本。 所有的资料?包括演讲稿?可以在这个网页上得到。

Below is a tentative list of topics. Each topic is expected to take one or two lectures.

• Overview of the theory of computation:
  Turing machines; The Church-Turing thesis; The traditional notions of computability, decidability, recursive enumerability; The fundamental limitations of algorithmic methods; Mapping reducibility; Turing reducibility; Kolmogorov complexity.

• Overview of classical logic:
  Propositional logic; Predicate (first-order) logic; The classical concepts of truth and validity; Hilbert- and Gentzen-style axiomatizations; The deduction theorem; Gödel's completeness theorem; Peano arithmetic; Gödel's incompleteness theorems.

• Games:
  Games as universal models of an agent's interaction with the environment; Static vs. dynamic games; Interactive Turing machines; Interactive computability; Interactive version of the Church-Turing thesis.

• Game operations:
  Negation; Choice operations; Blind operations; Parallel operations; Recurrence operations; Sequential operations.

• Computability and validity:
  The computational meanings of logical formulas; "Truth" as computability; Validity versus uniform validity.

• Deductive systems for computability logic:
  The propositional logics CL1 and CL2; The first-order logics CL3 and CL4; Affine logic; Intuitionistic logic.

• Applied theories based on computability logic:
  The advantages of such theories; The philosophy of constructivism; Computability-logic-based arithmetic.

• Knowledge base systems based on computability logic:
  Computability logic as a logic of knowledge; Computability logic as a declarative programming language; Resource-consciousness and constructiveness; Computability logic vs. epistemic logics.

• Systems for planning and action based on computability logic:
  The logic of tasks; Reflections on the frame and knowledge preconditions problems.

• Cirquent calculus:
  Linear logic; Shallow cirquent calculus; Abstract resource semantics; Deep cirquent calculus.

• Open problems and future directions:
  The need for developing better and richer syntax; Thoughts about a to-be-developed theory of interactive complexity; Potential applications in artificial intelligence - from theory to practice; A hot list of specific open problems.

Grading: A term paper should be submitted at the end of the semester, whose topic can be chosen by a student and approved by the instructor. Alternatively, a student may opt for taking a final examination instead of writing a term paper. The term paper or examination will contribute 50% toward your final grade. The remaining 50% will come from quizzes that will be given 5 to 10 times without warning, during the first 10-15 minutes of the class. Homework will be assigned after every meeting. It will not be collected or graded. However, the questions asked on a quiz will be typically based on (or be identical with) some questions from the latest 2 homework assignments. Students who listen actively, participate in discussions and volunteer answering questions may receive some extra credit at the time of deriving final grades.

评分标准? 学生在学期结束以前必须交一篇学期论文。题目可以由学生自己选择?再经过老师同意确定下来。另外?学生可以 选择参加学期考试代替学期论文。学期论文或者学期考试算学期分数的50%?其他的50%将由5-10次突然的小测试得到。这些小测试将在上课开始的10-15分钟进行。课外作业将在每次授课后布置?不需要上交?也不会评分?但是通常小测试中的问题会在前两次作业中出徍尽Ｑ�生在课堂上积极讨论、主动回答问题的?可以在学期末的评分中得到额外的分数。

---

Lecture notes

讲稿

NOTE: The following lecture notes are NOT copyrighted. Anyone in the world is permitted to copy and use them with or without modifications, and with or without acknowledging the source.

1. Introduction [6月19日]: What is computability logic. Computability logic versus classical logic. The current state of developement.

2. Mathematical preliminaries [6月19日]: Sets. Sequences. Functions. Relations. Strings.

3. Overview of the theory of computation [6月19日 - 6月21日]: Turing machines. The traditional concepts of computability, decidability and recursive enumerability. The limitations of the power of Turing machines. The Church-Turing thesis. Mapping reducibility. Turing reducibility. Kolmogorov complexity.

4. Classical propositional logic (quick review) [6月21日 - 6月26日]: What logic is or should be. Propositions. Boolean operations. The language of classical propositional logic. Interpretation and truth. Validity (tautologicity). Truth tables. The NP-completeness of the nontautologicity problem. Gentzen-style axiomatizations (sequent calculus systems).

5. Classical f irst-order logic (quick review) [6月26日 - 6月28日]: Propositional logic versus first-order (predicate) logic. The universe of discourse. Constants, variables, terms and valuations. Predicates as generalized propositions. Boolean operations as operations on predicates. Substitution of variables. Quantifiers. The language of first-order logic. Interpretation, truth and validity. The undecidability of the validity problem. A Gentzen-style deductive system. Soundness and Gödel's completeness.

6. Games [6月28日 - 7月3日]: Games as models of interactive computational tasks. Constant games. Prefixation. Traditional computational problems as games. Departing from functionality. Departing from the input-output scheme. Departing from the depth-2 restriction. Propositions as games. Not-necessarily-constant games. Games as generalized predicates. Substitution of variables in games.

7. Negation and choice operations [7月3日]: About the operations studied in computability logic. Negation. The double negation principle. Choice conjunction and disjunction. Choice quantifiers. DeMorgan's laws for choice operations. The constructive character of choice operations. Failure of the principle of the excluded middle for choice disjunction.

8. Parallel operations [7月3日 - 7月5日]: Parallel conjunction and disjunction. Free versus strict games. The law of the excluded middle for parallel disjunction. Resource-consciousness. Differences with linear logic. Parallel quantifiers. DeMorgan's laws for parallel operations. Evolution trees and evolution sequences.

9. Reduction [7月5日 - 7月10日]: The operation of reduction and the relation of reducibility. Examples of reductions. The variety of reduction concepts and their systematization in computability logic. Mapping reducibility is properly stronger than (simply) reducibility.

10. Blind quantifiers [7月10日]: Unistructurality. The blind universal and existential quantifiers. DeMorgan's laws for blind quantifiers. The hierarchy of quantifiers. How blind quantification affects game trees.

11. Recurrence operations [7月12日 - 7月17日]: What the recurrences are all about. An informal look at the main types of recurrences. The parallel versus branching recurrences. Formal definition of the parallel recurrence and corecurrence. Evolution sequences for parallel recurrences. Weak reductions. Weakly reducing multiplication to addition. Weakly reducing the RELATIVES problem to the PARENTS problem. Weakly reducing the Kolmogorov complexity problem to the halting problem. The ultimate concept of algorithmic reduction. Definition of the branching recurrence and corecurrence. Evolution sequences for branching recurrences. A look at some valid and invalid principles with recurrences.

12. Static games [7月17日]: Some intuitive characterizations of static games. Dynamic games. Pure computational problems = static games. Delays. Definition of static games.

13. Interactive computability [7月17日]: Hard-play machines. Easy-play machines. Definition of interactive computability. The interactive version of the Church-Turing thesis.

14. The language and formal semantics of computability logic [7月19日]: The formal language. Interpretations. Definitions of validity and uniform validity. Validity or uniform validity? The extensional equivalence between validity and uniform validity. Computability versus "knowability". Closure under Modus Ponens. Other closure theorems. Uniform-constructive closure.

15. Cirquent calculus [7月19日]: About cirquent calculus in general. The language of CL5. Cirquents. Cirquents as circuits. Formulas as cirquents. Operations on cirquents. The rules of inference of CL5. The soundness and completeness of CL5. A cirquent calculus system for classical logic. CL5 versus affine logic.

16. Logic CL4 [7月24日]: The language of CL4. The rules of CL4. CL4 as a conservative extension of classical logic. The soundness and completeness of CL4. The decidability of the blind-quantifier-free fragment of CL4. Other axiomatizations (affine and intuitionistic logics).

17. Applied systems based on computability logic [7月26日]: Computability logic as a problem-solving tool. Knowledgebase systems based on computability logic. Constructiveness, interactivity and resource-consciousness. Systems for planning and action based on computability logic. Applied theories based on computability logic. Computability-logic-based arithmetic.

---

Homework assignments

课外作业

---