观点线性时间逻辑
本文介绍提出的 Standpoint 逻辑,它是基于现有知识库语言的多模逻辑 “附加组件”,可用于表示相对不同、可能相冲突的立场的领域知识,并为具有不同表达能力的可判定一阶逻辑和描述逻辑提供决策算法,可扩展由立场建模。
Jun, 2022
本文中,我们引入了一种称为 Standpoint EL + 的扩展逻辑,它允许公理否定、角色链公理、自我循环等特性,并且通过设计一个满足可实际算法需求的可满足性检查演绎规则,同时保持了可处理性。我们通过展示该演绎规则的一个原型 Datalog 实现来证明实现的可行性。
Apr, 2023
本文提出了一种基于 Satisfiability Modulo Theories 的 Linear Temporal Logic 语言 ——LTLf Modulo Theories,该语言具有高表现力,可用于数据感知过程和规划的模型检验。我们提供了一种基于 SMT 编码的单遍树状表格系统的 LTLfMT 的半决策过程,并在黑色可满足检查工具中实现。实验结果表明了该算法在新型基准测试上的可行性。
Apr, 2022
本文针对 Temporal Equilibrium Logic(TEL)提供了一种系统的复杂性分析方法,可以检查 TEL 公式的时间均衡模型的存在性,并通过分析不同的 TEL 公式子类的复杂性,确定了可处理和不可处理的片段。
Feb, 2015
该论文介绍一种名为 Standpoint logic 的多透视角逻辑推理方法,并提出了一种基于嵌套序列演算的证明系统,利用多重颜色技术实现最坏情况复杂性最优的证明搜索算法。
May, 2022
介绍了一种名为 Standpoint EL 的多模态扩展版本,它允许相对于不同且可能相冲突的观点(或上下文)集成表示领域知识,具有轻量级描述逻辑的可解性,同时引入一些额外的功能使得标准的推理任务变得不可行。
Feb, 2023
本文探讨了线性时态逻辑(LTL)中,一类包括模态算子 F,G,X 和 U 的 Sahlqvist 公式具有一阶语言可定义的框架条件的对应关系。
Jun, 2022
本文探讨了神经符号计算中的两个基本问题:深度学习是否能够端到端地解决逻辑中的挑战性问题,以及神经网络是否能够学习逻辑的语义。研究重点是线性时间暂态逻辑(LTL),通过训练 Transformer 来直接预测给定 LTL 公式的解,使用传统求解器产生的经典解决方案生成训练数据,研究表明,使用这些特定的解决方案进行训练已足够。 Transformers 甚至可以预测在文献基准测试中,经典求解器超时的公式的解,它也可以推广到逻辑的语义,虽然与经典求解器找到的解有所不同,但仍可以正确地预测大多数公式的解。
Mar, 2020