AAAIDec, 2023

形式语言的最小基于宏的重写：理论与本体工程（及其扩展应用）

PDF
TL;DR该研究介绍了使用语法宏对有限形式语言进行重写的问题，提出了多项式时间算法来解决该问题的变体，并展示了其正确性。通过将算法应用于 OWL 编写的生物医学本体论，证明了该问题的实际相关性以及算法的可行性和有效性。此方法在提升本体质量和理解方面提供了有价值的帮助，并以系统的方式分析和评估重写系统的特性，包括语法宏、模板或其他形式的重写规则对计算问题的影响。
发现论文，激发创造
  • 计算描述逻辑本体的 Horn 重写

    将一个使用 DL L1 表达的本体 O1 重写为 Horn DL L2 中的本体 O2，以保证在任意数据集扩展时 O1 和 O2 是等价的。对存在 Horn 重写的本体进行研究，并识别出一类本体可以用多项式大小的 Horn 重写表示。

    Apr, 2015

  • 超越 Horn 本体的 Datalog 重写计算

    本文研究了非 Horn 本体的查询方法，使用 datalog 重写来回答 OWL 2 DL 本体查询的可能性等问题，并提出了一种基于分辨率的过程来解决 SHI 本体问题。

    Apr, 2013

  • 本体查询：重写与优化 (扩展版)

    本文研究了本体查询中的查询重写和查询优化问题，其中查询重写包括将本体查询编译为与底层关系型数据库等效的查询，查询优化旨在改善此过程以生成成本效益高的 UCQ 重写，提出了一种有效的新方法以支持基于线性 Datalog+/- 的规则。

    Dec, 2011

  • 基于自动正式化的数学和代码正确性研究：基础证明实验

    本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

    Jan, 2023

  • 非确定性代数重写为伴随

    提出一般模型理论语义学来处理重写，利用预排序代数模型理论来处理具有不同排序的代数。在这个框架下，将重写在任意代数上进行特征化，使用该结果证明了基于非确定性编程的 Maude 和 CafeOBJ 的抽象计算模型的声音和完整性，并在 pushout-based 模块化技术的上下文中为代数重写开发了组成性结果。

    Apr, 2022

  • 证明结构研究

    提出并阐述了一种新的证明操纵和分析形式主义，为证明检索方式提高了效率，实现了较短证明的自动化，特别是在首阶问题上的历史证明中进行了一项全面的形式重建分析。

    Feb, 2023

  • 命题框架中优化的抽象视角

    提出了一种名为权重系统的统一框架，该框架消除了自动推理和知识表示中的语法差异，并解释了不同范例所提供的优化语句之间的异同，从而方便了翻译程序的开发和证明了不同框架的形式属性。

    Jun, 2022

  • 宏语法及整体触发在有效语义解析中的应用

    该研究提出了一种新的在线学习算法，利用宏语法缓存已发现的有用逻辑形式的抽象模式，以及利用整体触发根据句子相似度高效检索相关模式，其在 WikiTableQuestions 数据集上达到 43.7% 的准确率和 11 倍的速度提升。

    Jul, 2017

  • 非布尔形式主义优化统一框架

    该论文提出了一种名为扩展权重系统的统一框架，可消除不同自动推理语言之间的句法区别，并研究了所提出系统的形式属性，即可在该框架内捕获的范例的形式属性。

    Jun, 2022

  • 神经网络能学会符号重写吗？

    本文研究当前神经结构对于学习符号重写的充分性，并提出了两种数据集。使用当前的神经机器翻译模型进行实验，并讨论了其结果。本研究的相关性得到了验证，同时提出了拓展该研究的思路。

    Nov, 2019