摘要： 计算机科学的很多领域引入了形式化方法，逻辑公式经常出现在各种技术中。有时需要判定一个逻辑公式的协调性可满足性。并对可满足的公式给出一个具体的模型。本文介绍计算机科学和数学中的一些模型构造问题。以及有限模型的自动构造技术。

关键词: 计算机科学 有限模型 自动构造