一种基于TLA的解决N皇后问题的方法

• 作者: 台亚非 龙士工
• 来源期刊: 贵州大学学报（自然科学版）
• 学科: 工学
• 关键词: 行为时序逻辑 模型检测 N皇后问题 Toolbox
• 年，卷（期）: 2016,（1）
• 所属期刊栏目: ?工程科学研究及应用? -- 计算机技术
• 页码范围: 86-88
• 页数: 3页
• 分类号: TP301
• 字数: 2361字
• 语种: 中文
• DOI: 10.15958/j.cnki.gdxbzrb.2016.01.20

摘要

行为时序逻辑语言( TLA＋)是一种在模型检测范围内能够表达模型程序和逻辑规约的语言。 N皇后问题是一个久远的问题，回溯法是解决该问题一种经典的方法。本文提出如何用行为时序逻辑语言TLA＋去描述N皇后问题，然后使用Toolbox工具去检测n=5时该问题的全部解。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	龙士工	贵州大学计算机科学与信息学院	39	110	5.0	9.0
2	台亚非	贵州大学理学院	1	0	0.0	0.0