首页> 外文会议>Automated reasoning with analytic tableaux and related methods >A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules
【24h】

A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules

机译:基于命题Tableaux的带默认规则推理的证明演算

获取原文
获取原文并翻译 | 示例

摘要

Since introduced by Reiter in his seminal 1980 paper: 'A Logic for Default Reasoning', the subject of reasoning with default rules has been extensively dealt with in the literature on nonmonotonic reasoning. Yet, with some notable exceptions, the same cannot be said about its proof theory. Aiming to contribute to the latter, we propose a tableaux based proof calculus for a propositional variant of Reiter's presentation of reasoning with default rules. Our tableaux based proof calculus is based on a reformulation of the semantics of Reiter's view of a default theory, i.e., a tuple comprised of a set of sentences and a set of default rules, as a premiss structure. In this premiss structure, sentences stand for definite assumptions, as normally found in the literature, and default rules stand for tentative assumptions, as opposed to rules of inference, as normally found in the literature. On this basis, a default consequence is defined as being such relative to a premiss structure, as is our notion of a default tableaux proof. In addition to its simplicity, as usual in tableaux based proof calculi, our proof calculus allows for the discovery of the non-existence of proofs by providing corresponding counterexamples.
机译:自从Reiter在其1980年的开创性论文“默认推理的逻辑”中提出以来,使用默认规则进行推理的主题已在有关非单调推理的文献中得到了广泛处理。但是,除了一些明显的例外,关于其证明理论也不能说相同的话。为了为后者做出贡献,我们针对Reiter的默认规则推理的命题变体提出了一种基于表格的证明演算。我们基于表格的证明演算是基于Reiter的默认理论视图语义的重新表述,即,由一组句子和一组默认规则组成的元组作为前提结构。在这种前提结构中,句子代表文献中通常发现的确定假设,默认规则代表暂定假设,与文献中通常发现的推论规则相反。在此基础上,默认后果被定义为相对于前提结构而言,就像我们对默认表格证明的概念一样。除了其简单性(如在基于Tableaux的证明计算中通常使用的那样)之外,我们的证明演算还可以通过提供相应的反例来发现证明的不存在。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号