首页> 外文期刊>Journal of logic and computation >On the formal characterization of the FORTE_MBC theory revision operators
【24h】

On the formal characterization of the FORTE_MBC theory revision operators

机译:关于FORTE_MBC理论修订运算符的形式化表征

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

摘要

FORTE_MBC is a First-Order Logic theory revision system, built upon the FORTE system but with an important supplement: it makes use of (i) a Bottom Clause to define the search space of literals and (ii) a set of mode declarations to validate the yielded clauses. Introducing the Bottom Clause was essential to reduce the runtime of the revision process (experimental results showed an average speed-up of 55x), since one of the key steps of the revision process is to create literals to add to clauses. However, the effectiveness and efficiency of learning and revising as a refinement process heavily rely on other factors, such as the generality relation that induces a generalization model for the search space, and, as a consequence, the refinement operators. These components have never been formally analysed in FORTE(_MBC). In this work, we contribute with (i) an adaptation of the existing theoretical frameworks that characterize refinement operators to define the search space and revision operators of systems like FORTE_MBC, which use a set of Bottom Clauses and mode declarations to constrain the search; (ii) an improvement of the theory refinement operators of FORTE_MBC to make them ideal for the defined space. We present the feasibility of these modified operators by implementing them in the FORTE_MBC system. Experimental results show that we are indeed able to obtain a more efficient revision process by using the proposed ideal operators.
机译:FORTE_MBC是基于FORTE系统构建的一阶逻辑理论修订系统,但有一个重要的补充:它利用(i)底部子句定义文字的搜索空间,以及(ii)一组用于验证的模式声明产生的子句。引入Bottom子句对于减少修订过程的运行时间至关重要(实验结果显示平均速度提高了55倍),因为修订过程的关键步骤之一是创建要添加到子句中的文字。但是,作为优化过程的学习和修订的有效性和效率在很大程度上取决于其他因素,例如为搜索空间引入泛化模型的泛化关系,以及因此而导致的优化运算符。这些组件从未在FORTE(_MBC)中正式分析过。在这项工作中,我们做出了以下贡献:(i)对现有理论框架进行改编,这些理论框架表征精化运算符以定义诸如FORTE_MBC之类的系统的搜索空间和修订运算符,后者使用一组Bottom子句和模式声明来约束搜索; (ii)FORTE_MBC的理论细化运算符的改进,使其非常适合定义的空间。通过在FORTE_MBC系统中实现它们,我们介绍了这些修改后的运算符的可行性。实验结果表明,通过使用建议的理想运算符,我们确实能够获得更有效的修订过程。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号