The Wayback Machine - https://web.archive.org/web/20221029033827/https://baike.sogou.com/kexue/d10175.htm

计算机科学中的逻辑

编辑
计算机逻辑门图解表示

计算机科学中的逻辑涵盖了逻辑领域和计算机科学领域之间的重叠。该主题基本上可以分为三个主要领域：

  • 理论基础和分析
  • 利用计算机技术帮助逻辑学家
  • 计算机应用中逻辑概念的使用

1 理论基础和分析编辑

逻辑在计算机科学中起着基础性的作用。逻辑中一些特别重要的关键领域是可计算性理论(以前称为递归理论)、模态逻辑和范畴理论。计算理论是基于逻辑学家和数学家如阿隆佐·邱奇和艾伦·图灵定义的概念。[1][2] 丘奇首先用他的λ可定义性概念证明了算法上不可解决的问题的存在。图灵对所谓的机械过程进行了第一次令人信服的分析，库尔特·哥德尔断言他发现图灵的分析“完美无缺”。[3]此外，逻辑和计算机科学之间理论重叠的其他一些主要领域是：

  • 哥德尔的不完全性定理证明，任何足以描述算术的逻辑系统都将包含在该系统中既不能被证明也不能被否定的语句。这直接应用于与证明软件完整性和正确性的可行性相关的理论问题。[4]
  • 框架问题是用一阶逻辑表示人工智能主体的目标和状态时必须克服的基本问题。[5]
  • 柯里-霍华德对应关系是逻辑系统和软件之间的关系。这个理论在证明和程序之间建立了精确的对应关系。特别地，它表明简单类型λ演算中的项对应于直觉命题逻辑的证明。
  • 范畴理论代表了强调结构之间关系的数学观点。它与计算机科学的许多方面密切相关：编程语言的类型系统、转换系统理论、编程语言模型和编程语言语义学理论。[6]

2 帮助逻辑学家的计算机编辑

最早使用人工智能这个术语的应用之一是由艾伦·纽厄尔、肖和希尔伯特·西蒙在1956年开发的逻辑理论家系统。逻辑学家所做的事情之一是在逻辑中取一组语句，并根据逻辑定律推导出必须为真的结论(附加语句)。例如，如果给定一个逻辑系统，陈述“所有人都是凡人”和“苏格拉底是凡人”，一个有效的结论是“苏格拉底是凡人”。当然，这是一个简单的例子。在实际的逻辑系统中，语句可能是众多而复杂的。人们很早就意识到计算机的使用可以使这种分析得到很大的帮助。逻辑理论家系统在伯特兰·罗素和阿尔弗雷德·诺斯·怀特海对数学逻辑有影响的著作《数学原理》中验证了他们的理论工作。此外，逻辑学家利用后续系统来验证和发现新的逻辑定理和证明。[7]

3 计算机的逻辑应用编辑

数学逻辑对人工智能领域一直有很大的影响。从该领域开始，人们就认识到，自动化逻辑推理的技术在解决问题和从事实中得出结论方面具有巨大潜力。罗恩·布拉克曼(Ron Brachman)将一阶逻辑(FOL)描述为所有人工智能知识表示形式都应该被评估的度量标准。没有比FOL更通用或更强大的描述和分析信息的已知方法了。FOL本身之所以没有被用作计算机语言，是因为它实际上表达能力太强，也就是说FOL可以很容易地表达任何计算机，无论多么强大，都无法解决的语句。因此，在某种意义上，每种形式的知识表示都是可表达性和可计算性之间的权衡。语言表达得越多，越接近FOL，就越有可能变慢，并倾向于无限循环。[8]

例如，专家系统中使用的“IF THEN”规则接近于FOL的一个非常有限的子集。逻辑学家称之为Modus Ponens，而不是具有全部逻辑运算符的任意公式。因此，基于规则的系统可以支持高性能计算，特别是当它们利用优化算法和编译时。[9]

逻辑理论的另一个主要研究领域是软件工程。基于知识的软件助手和程序员学徒程序等研究项目应用逻辑理论来验证软件规范的正确性。他们还使用它们将规范转换成不同平台上的高效代码，并证明实现和规范之间的等价性。[10] 这种形式转换驱动的方法通常比传统的软件开发更加有效。然而，在具有适当形式和可重用模板的特定领域，该方法已被证明对商业产品是可行的。合适的领域通常是武器系统、安全系统和实时金融系统，其中系统故障会造成过高的人力或财务成本。这一领域的一个例子是超大规模集成电路设计——设计用于数字设备的中央处理器和其他关键部件的芯片的过程。芯片中的错误是灾难性的。与软件不同，芯片不能被修补或更新。因此，使用形式化方法来证明实现符合规范是有商业理由的。[11]

逻辑在计算机技术中的另一个重要应用是框架语言和自动分类器领域。像KL-ONE这样的框架语言有严格的语义。KL-ONE中的定义可以直接映射到集合论和谓词演算。这允许称为分类器的专门定理证明器分析给定模型中集合、子集和关系之间的各种声明。通过这种方式，可以验证模型，并标记任何不一致的定义。分类器还可以推断新信息，例如基于现有信息定义新集合，并基于新数据改变现有集合的定义。这种灵活性非常适合处理不断变化的互联网世界。分类器技术建立在诸如网络本体语言之类的语言之上，以允许在现有的互联网上实现逻辑语义级别。这一层叫做语义网。[12][13]

时态逻辑用于并发系统中的推理。[14]

参考文献

  • [1]

    ^Lewis, Harry R.; Christos H. Papadimitriou (1981). Elements of the Theory of Computation. Englewood Cliffs, New Jersey: Prentice-Hall. ISBN 0-13-273417-6..

  • [2]

    ^Davis, Martin. "Influences of Mathematical Logic on Computer Science". In Rolf Herken. The Universal Turing Machine. Springer Verlag. Retrieved 26 December 2013..

  • [3]

    ^Kennedy, Juliette. Interpreting Godel. Cambridge University Press. Retrieved 17 August 2015..

  • [4]

    ^Hofstadter, Douglas R. Gödel, Escher, Bach: An Eternal Golden Braid. Basic Books. ISBN 978-0465026562..

  • [5]

    ^McCarthy, J; P.J. Hayes (1969). "Some philosophical problems from the standpoint of artificial intelligence". Machine Intelligence. 4: 463–502..

  • [6]

    ^Barr, Michael; Charles Wells (1990). Category Theory for Computer. Prentice-Hall..

  • [7]

    ^Newell, Allen; J.C. Shaw; H.C. Simon (1963). "Empirical explorations with the logic theory machine". In Ed Feigenbaum. Computers and Thought. McGraw Hill. pp. 109–133. ISBN 978-0262560924..

  • [8]

    ^Levesque, Hector; Ronald Brachman (1985). "A Fundamental Tradeoff in Knowledge Representation and Reasoning". In Ronald Brachman and Hector J. Levesque. Reading in Knowledge Representation. Morgan Kaufmann. p. 49. ISBN 0-934613-01-X. The good news in reducing KR service to theorem proving is that we now have a very clear, very specific notion of what the KR system should do; the bad new is that it is also clear that the services can not be provided... deciding whether or not a sentence in FOL is a theorem... is unsolvable..

  • [9]

    ^Forgy, Charles (1982). "Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem*" (PDF). Artificial Intelligence. 19: 17–37. doi:10.1016/0004-3702(82)90020-0. Archived from the original (PDF) on 2013-12-27. Retrieved 25 December 2013..

  • [10]

    ^Rich, Charles; Richard C. Waters (November 1987). "The Programmer's Apprentice Project: A Research Overview" (PDF). IEE Expert Special Issue on the Interactions between Expert Systems and Software Engineering. Retrieved 26 December 2013..

  • [11]

    ^Stavridou, Victoria (1993). Formal Methods in Circuit Design. Press Syndicate of the University of Cambridge. ISBN 0-521-443369. Retrieved 26 December 2013..

  • [12]

    ^MacGregor, Robert (June 1991). "Using a description classifier to enhance knowledge representation". IEEE Expert. 6 (3): 41–46. doi:10.1109/64.87683. Retrieved 10 November 2013..

  • [13]

    ^Berners-Lee, Tim; James Hendler; Ora Lassila (May 17, 2001). "The Semantic Web A new form of Web content that is meaningful to computers will unleash a revolution of new possibilities". Scientific American. 284: 34–43. doi:10.1038/scientificamerican0501-34. Archived from the original on April 24, 2013..

  • [14]

    ^Colin Stirling (1992). "Modal and Temporal Logics". In S. Abramsky; D. M. Gabbay; T. S. E. Maibaum. Handbook of Logic in Computer Science. II. Oxford University Press. pp. 477–563. ISBN 0-19-853761-1..

阅读 90
版本记录

  • 暂无