Computer-Aided Reasoning
Computer-Aided Reasoning
复制标题
计算机辅助推理
DOI：
10.1007/978-1-4757-3188-0
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
M. Hinchey
中科院分区：
文献类型：
--
作者：
M. Hinchey
我们定义了一个函数，该函数找到给定有向图的两个给定节点之间的路径，如果这样的路径存在的话。我们证明了函数终止，我们证明了它是正确的。除了说明一种在ACL 2中形式化有向图的方法外，本章还说明了用户将问题分解为数学上易于处理的部分的重要性，以及定义新概念以形式化这些部分的重要性。我们的证明涉及到这样的辅助概念，作为一个简单的（无环）路径，从任意路径获得一个简单的路径的过程中，收集所有简单路径的算法。我们分析的算法是一个天真的，执行时间指数的边缘数。本章不需要图论的专业知识;事实上，本章的主要内容与图论无关。它们是：发展您的形式化技能，并细化您对形式化将涉及的内容的期望。对项目的适当期望往往是成功的关键。
We define a function that finds a path between two given nodes of a given directed graph, if such a path exists. We prove the function terminates and we prove that it is correct. Aside from illustrating one way to formalize directed graphs in ACL2, this chapter illustrates the importance of the user's decomposition of a problem into mathematically tractable parts and the importance of defining new concepts to formalize those parts. Our proof involves such auxiliary notions as that of a simple (loop-free) path, the process for obtaining a simple path from an arbitrary path, and an algorithm for collecting all simple paths. The algorithm we analyze is a naive one that executes in time exponential in the number of edges. This chapter requires no specialized knowledge of graph theory; indeed, the main thrusts of the chapter have nothing to do with graph theory. They are: to develop your formalization skills and to refine your expectations of what a formalization will involve. Appropriate expectations of a project are often the key to success.