摘要
为变量受约束理论约束的子句引入一种消解原理的约束逻辑方法。约束可看成量词限制，滤去那些约束理论的任何解释都可指定给带有这样的限定量词公式的变量值。本文提出了一种约束子句的消解原理，其中测试是否满足约束理论的约束取代了一致化。研究表明，如果约束子句集不满足约束理论当且仅当对约束理论的每一模型，能推出一约束空子句，而该空子句的约束在模型中是可满足的。
The author introduces a constrained logic scheme with a resolution principle for clauses whose variables are constranied by a constraint theory. Constraints can be seen as quantifier restrications filting out the values that any interpretation of the underlying constraint theory can assign to the variables of a formula with such restricted quantifiers. A resolution principle for constrained clauses is proposed, where unification is replaced by testing constraints for satisfiability over the constraint theory. It is shown that constrained resolution is sound and complete, in that a set of constrained clauses is unsatisfiable over the constraint throry, if and only if for each model of th constraint theory, and constrained empty clause whose constraint is satisfiable.
