论文标题
通过定理合成直觉命题逻辑中的绑架推理
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
论文作者
论文摘要
借助于直觉命题逻辑的基于紧凑的基于序言的定理谚语，我们合成了最小的假设，在该假设下，给定的公式为定理。 将我们的合成算法应用于涵盖基本的绑架推理机制之后，我们综合了文字的结合，以模仿经典或中级逻辑中的真实表的行，并且我们将有条件的假设纳入了将古典或中间逻辑的定理转化为直觉上的理论的理论。更进一步，我们将绑架性推理机制推广到使用最小的规范公式集合更具表现力的序列前提来合成更具表现力的序列前提，从而可以减少积极中的任意公式，同时保留其可证明性。 本文是一个独立的识字序言计划，支持对其内容的交互式探索，并确保我们的结果充分可复制性。
With help of a compact Prolog-based theorem prover for Intuitionistic Propositional Logic, we synthesize minimal assumptions under which a given formula formula becomes a theorem. After applying our synthesis algorithm to cover basic abductive reasoning mechanisms, we synthesize conjunctions of literals that mimic rows of truth tables in classical or intermediate logics and we abduce conditional hypotheses that turn the theorems of classical or intermediate logics into theorems in intuitionistic logic. One step further, we generalize our abductive reasoning mechanism to synthesize more expressive sequent premises using a minimal set of canonical formulas, to which arbitrary formulas in the calculus can be reduced while preserving their provability. Organized as a self-contained literate Prolog program, the paper supports interactive exploration of its content and ensures full replicability of our results.
