A Tableau Calculus for Minimal Model Reasoning
A Tableau Calculus for Minimal Model Reasoning
复制标题
用于最小模型推理的 Tableau 演算
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
I. Niemelä
中科院分区：
文献类型：
--
作者：
I. Niemelä
本文研究了极小模型推理的自动化，即判定一个公式在前提的每个极小模型中是否成立。分两步提出了一种新的用于命题最小模型推理的Tableau演算。首先介绍了一种采用限制割规则的解析子句表演算。然后利用极小模型的落地性将演算扩展到处理极小模型推理。设计了一个基于基本演算的决策过程，并将其推广到最小模型推理。基本决策过程及其扩展具有一些有趣的性质。在确定逻辑推理时，基本过程是优先于最小模型来探索反模型的搜索空间，并且每个反模型不会生成一次以上。该程序可以在多项式空间中运行，并为Horn子句提供了多项式时间判决过程。扩展的决策过程也可以用来寻找一组子句的所有极小模型。
The paper studies the automation of minimal model inference, i.e., determining whether a formula is true in every minimal model of the premises. A novel tableau calculus for prepositional minimal model reasoning is presented in two steps. First an analytic clausal tableau calculus employing a restricted cut rule is introduced. Then the calculus is extended to handle minimal model inference by employing a groundedness property of minimal models. A decision procedure based on the basic calculus is devised and then it is extended to minimal model inference. The basic decision procedure and its extension enjoy some interesting properties. When deciding logical consequence, the basic procedure explores the search space of counter-models with a preference to minimal models and each counter-model is not generated more than once. The procedures can be implemented to run in polynomial space, and they provide polynomial time decision procedures for Horn clauses. The extended decision procedure can also be used to finding all minimal models of a set of clauses.