| 有限模型生成及其应用 |
| 张健
|
| 1994
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 摘要 | 本论文主要研究有限模型自动生成的技术及其应用。模型生成是指给定一个逻辑公式（或一组逻辑公理），自动地构造出它的有限模型。从理论上讲，自动构模的复杂度太高，因而限制了其应用。但是在某些实际应用中，它仍然是可行的。这篇论文主要是研究提高模型生成器效率的技术，并探索这类工具的应用。针对小理论，发展了一种在搜索空间中消除同构的方法。它可以大大提高构模的效率。基于这种消除同构的方法，我们实现了一个程序。实验结果表明，该程序在很多代数问题上效率较高。解决一些数学问题。 |
| 其他摘要 | This thesis is concerned with the techniques and applications of finite model generation. Model generation means the automated construction of models of a given logical formula. Theoretically speaking, automatic model generation suffers from high complexity and can find few applications. But in practice, it may be feasible in some cases. |
| 页数 | 52
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/6242
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
张健. 有限模型生成及其应用[D]. 中国科学院软件研究所. 中国科学院软件研究所,1994.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论