根据给定的文件信息，我们可以整理出以下知识点：
标题《论文研究-Model Checking Go.pdf》暗示了文档内容与围棋游戏以及模型检测技术（Model Checking）相关。模型检测是一种用于验证有限状态系统的自动技术。围棋是一种古老且复杂的棋类游戏，具有高度的复杂性和策略性。文档标题表明研究的重心在于如何将模型检测应用于围棋游戏的分析和策略制定。
描述中提到的“基于符号模型检测的围棋方法与基于学习的方法有互补性”说明了文档将探讨两种不同的AI方法在围棋游戏中应用时的相互补充作用。符号模型检测方法可能依赖于明确的规则和状态空间的详细表示，而学习方法，尤其是深度学习，可能通过经验来提高决策能力，这两种方法结合起来，可以提高围棋策略的效率和准确性。
文件中提到了朱维军这个名字，可能是文章的作者或者研究者的名字。作者属于郑州大学信息工程学院（School of Information Engineering, Zhengzhou University），这给出了研究机构的背景信息。
在内容摘要部分，“The Goalgorithm based on symbolic model checking and the one based on deep learning are complementary”揭示了文档要讨论的核心主题：符号模型检测和深度学习算法如何在围棋游戏中相互补充。作者提出了一种新的算法来解决围棋游戏，通过先获取一个限制条件强的保守版本算法，然后放松条件，得到一个更为激进的算法版本。这种方法通过案例研究展示，新算法在某些情况下比现有技术做得更多。这种新算法可能涉及到条件的放宽以及对策略的优化。
摘要中还提到了在2016年3月进行的一场人机围棋赛，职业九段棋手李世石与名为AlphaGo的著名围棋程序对战。这场比赛吸引了全世界的关注，并且AlphaGo出人意料地以四胜一负的成绩胜出，这标志着人工智能在围棋领域取得的巨大进步。这一事件也印证了文档内容将探讨的内容。
“Time complexity of Go problem has been proved to be EXPTIME”这一句揭示了围棋问题的时间复杂性，也就是说，围棋游戏的状态空间非常庞大，按照计算复杂性理论，围棋的时间复杂度被证明为EXPTIME。这意味着，无法通过穷尽搜索所有的状态来解决问题，这也突出了为什么需要开发更高效的算法来处理围棋游戏。
“Alpha-Go program by the combination of deep learning, reinforcement learning and Monte Carlo tree search”指的是DeepMind公司在2016年发表的AlphaGo程序。AlphaGo将深度学习、强化学习和蒙特卡洛树搜索相结合，形成了一种不同于传统模型检测方法的围棋AI。这种结合了多种AI技术的方法不需要保证每次移动都采取最佳策略，而是通过大量人类专家的比赛和自我对弈提供概率计算和游戏树剪枝的基础，参与到深度神经网络的大规模样本训练中。
此外，内容还提到了“pruningsomebrancheswhicharealmostimpossibletowininthegametree,bringsmuchefficiency”这段话表明，通过剪枝（即减少搜索空间）可以大幅提高效率，但也可能在某些情况下导致信息的丢失。这可能是新算法试图解决的问题之一，即如何在剪枝以提高效率的同时，尽量减少信息丢失。
文档中出现了一些扫描错误和遗漏，表明内容并非完全准确无误。不过，通过上下文的联系和逻辑推断，我们仍可以对文档的中心思想有一个清晰的理解。整体来说，文档讨论了将符号模型检测与深度学习方法相结合的新算法，并通过案例研究说明该算法在围棋游戏中的优势和可能的不足。
