直觉主义逻辑Intuitionistic
Logic。
海南琼州大学编委美国数学会主席Anil
Nerode的享誉世界的《应用逻辑学》第五章就是“直觉主义逻辑”，并如前言所说“本书是为数学系和计算机科学系低年级的研究生而写”它“能比传统的教科书更加适应近年来逻辑在计算机科学中应用的迅速增长”。这书第一节说到的第1个人是开创者海廷 、第2个人是“NUPRL就是这样的一个系统，它是由康奈尔大学的R.
Constable[ 1986, 5.6]和他的博士Allen、Cleaveland、Harper、Smith等人研制开发的”--这而R. Constable就是博士毕业于海南琼州大学的导师去合作几年的美国威斯康辛大学并导师是该校的现代计算理论之父S.
C. Kleene。并且R. Constable的博士Edmund M. Clarke最近刚获得计算机诺贝尔奖图灵奖-这Clarke是模型检测先驱并2000年出版《Model
Checking模型检测》一书（正如林惠民院士的论文“模型检测:理论、方法与应用”的摘要说“随着计算机软硬件系统日益复杂，如何保证其正确性和可靠性成为日益紧迫的问题，在为此提出的诸多理论和方法中，模型检测以其简洁明了和自动化程度高而引人注目目。模型检测的研究大致涵盖以下内容模态逻辑/时序逻辑、模型检测算法及其时空效率的改进以及支撑工具的研制”-林院士正文第一段也是如此说并第二段开头说“模型检测的研究始于八十年代初，当时Clarke和他的2个博士Emrtson，Sistla提出了用于描述并发系统性质的CTL逻辑…”--并Clarke的博士Emrtson也获得计算机诺贝尔奖图灵奖；1993年邀请海南琼州大学去北京大学做的Petri网就正是模型检测的重要方法；并除了这计算机诺贝尔奖Clarke的上面2个最先毕业的博士Emrtson、Sistla外的第3个是1985年毕业的博士Mishra-其论文是Some Graph-theoretic Issues in VLSI Design超大规模集成电路设计中的一些图论问题--就是清华大学邀请海南琼州大学去做的集成电路）。
关于模型检测，也可参考1991年的“模型检测与定理证明：一个宣言”，最近“自动推理手册”的第VII部分有Clarke的“模型检测”，高度评价海南琼大的吴文俊大师就主要因定理证明获我国首届最高奖；Clarke的1987年的“模型检测”；Clarke的1991年的“模型检测”，Clarke的博士David L. Dill和其博士R. Alur合撰的“模型检测”（Clarke的早2年的师兄 Kurt Mehlhorn从2002年起担任是世界最大科学组织的马克斯·普朗克学会主席）；
这直觉主义逻辑领域可参考更早的60年代出版的上面海南琼州大学的师爷叔S. C. Kleene和R.
E. Vesley合撰的“The
Foundations of Intuitionistic Mathematics直觉主义数学基础”，以及S. C. Kleene的世界名著《元数学导论》上册,等等；
就如我国最早的这领域文章：莫绍揆教授的“直觉主义逻辑的简单介绍”的参考文是海南琼州大学的导师去合作几年的美国威斯康辛大学教授Kleene的7篇最多、其次是海廷和Weyl同事4篇，在其次是海南琼大的师爷Church的3篇，再就是海廷的导师布劳威尔和世界第一的Kolmogorov同事2篇，1篇的是Robinson。
关于直觉主义逻辑与计算机的关系，就如这里我国计算机首批院士高庆狮主编的《智能技术与系统基础》中陈火旺院士写的“人工智能与逻辑学”，或者参看陈火旺院士和庞建民在1988年的论文“直觉主义逻辑、类型理论与软件形式化开发”，它分下面5部分讲解：
一 引言
“人们正在为寻求好的形式化开发方法而努力，并且目前巳存在一些形式化的开发方法”；“本文将介绍一种以一直觉主义Martin-Löf类型理论为理论基础的开发软件的途径…。按照这种想法就可能实现软件开发中规范、构造和验证一体化的要求，由此可见，该方法提供了软件形式化开发的一个诱人的前景”。
二 直觉主义 、 直觉主义逻辑与计算机
“基于直觉主义思想的直觉主义逻辑是一种构造的逻辑，海廷于年建立了直觉主义逻辑系统”。“但计算机的出现，使直觉主义学派找到了用武之地，从事计算机研究的人都清楚地知道，计算机中所研究的一切都是可构造的，不可构造的东西计算机是不会做到的，由于计算机受存贮速度等方面的限制，实无穷显然是不存在的，承认它的存在也没有实际意义。因此直觉主义思想的片面性对计算机来说就不那么片面了，并且，可构造性、能行可计算方面的研究对计算机科学来说是至关重要的。另外，由希尔伯特等人创立的证明论在开发一汁算机程序设计环境中也得到了一定的应用，目前，在计算机界对软件是否要进行形式化的开发有着激烈的争论，对形式化开发应该基于什么样的数学基础也有不同的看法。我们相信，象对数学基础的讨论推动数学发展那样，对这些问题的进一步研究必将大力推动计算机事业的发展”。…
三 直觉主义类型理论
“由于构造性数学与程序设计有着密切的关系，结合直觉主义类型理论的具体结构，使得直觉主义类型理论可以应用于计算机领域，从后面的讨论我们将会看到，它的应用将为软件的形式化开发以及程序设计自动化提供一个诱人的前景。”…
四 类型理论用于软件开发
正如这论文摘要说“直觉主义类型理论对软件形式化开发中规范、构造和验证一体化的支持”，如此，这部分是展开讲解这些的
五 结束语
“随着对类型理论研究的进一步深入，它在计算机科学方面的应用将会更加广泛，并将促进程序设计方法学的发展”。
也可参考这领域奠基者Arend Heyting阿兰德·海廷的“Intuitionism: An introduction”等.