论文部分内容阅读
为变量受约束理论约束的子句引入一种消解原理的约束逻辑方法。约束可看成量词限制，滤去那些约束理论的任何解释可指定给带有这样的限定量词公式的变量值。本文提出一种约束子句的消解原理，其中测试是否满足约束理论的约束取代了一致化。研究表明，如果约束子句集不满足的约束理论当且仅当对约束理论的每一模型，能推出一约约束空子句，而该空子句的约束在模型中是可满足的，那么约束是合理的和完备的。