论文标题
超越公式 - 符合形象：布尔逻辑到任意图的扩展
Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
论文作者
论文摘要
我们提出了一个基于图的布尔逻辑扩展名，称为布尔图逻辑（BGL）。将公式树解释为Cographs的Cotrees，我们可能会用纯图理论术语来陈述语义概念，例如评估和构成，从中我们恢复了BGL的定义。自然，这对通常的布尔逻辑是保守的。 我们的贡献如下： （1）我们基于布尔关系提供了BGL的自然语义，即它是一种多相的语义，并显示了该语义对相应综合概念的足够性。 （2）我们表明，评估的复杂性对于任意图（而不是公式的alogtime-complete）是NP的完整性，而元素为$π^p_2 $ complete（与公式的conp-complete相反）。 （3）我们给出了一种“递归”算法，用于通过诱导图的模块化分解来评估。 （尽管这不是多项式时间，请参见上面的第（2）点）。 （4）我们在游戏理论环境中表征了评估，从静态策略和序列策略方面，扩展了位置游戏的经典概念，而不是Cographs。 （5）我们给出了BGL的公理化，灵感来自深入的证明理论，并显示了相应的综合概念的健全性和完整性。 One particular feature of the graph-theoretic setting is that it escapes certain no-go theorems such as a recent result of Das and Strassburger, that there is no linear axiomatisation of the linear fragment of Boolean logic (equivalently the multiplicative fragment of Japaridze's Computability Logic or Blass' game semantics for Mutliplicative Linear Logic).
We propose a graph-based extension of Boolean logic called Boolean Graph Logic (BGL). Construing formula trees as the cotrees of cographs, we may state semantic notions such as evaluation and entailment in purely graph-theoretic terms, whence we recover the definition of BGL. Naturally, it is conservative over usual Boolean logic. Our contributions are the following: (1) We give a natural semantics of BGL based on Boolean relations, i.e. it is a multivalued semantics, and show adequacy of this semantics for the corresponding notions of entailment. (2) We show that the complexity of evaluation is NP-complete for arbitrary graphs (as opposed to ALOGTIME-complete for formulas), while entailment is $Π^p_2$-complete (as opposed to coNP-complete for formulas). (3) We give a 'recursive' algorithm for evaluation by induction on the modular decomposition of graphs. (Though this is not polynomial-time, cf. point (2) above). (4) We characterise evaluation in a game-theoretic setting, in terms of both static and sequentical strategies, extending the classical notion of positional game forms beyond cographs. (5) We give an axiomatisation of BGL, inspired by deep-inference proof theory, and show soundness and completeness for the corresponding notions of entailment. One particular feature of the graph-theoretic setting is that it escapes certain no-go theorems such as a recent result of Das and Strassburger, that there is no linear axiomatisation of the linear fragment of Boolean logic (equivalently the multiplicative fragment of Japaridze's Computability Logic or Blass' game semantics for Mutliplicative Linear Logic).
