Satoshi Matsuoka
In this paper, we give a new linear time correctness condition for proof nets of Multiplicative Linear Logic without units. Our approach is based on a rewriting system over trees. We have only three rewrite rules. Compared with previous linear time correctness conditions, our system is surprisingly simple and intuitively appealing.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We prove a completeness result for Multiplicative Exponential Linear Logic (MELL): we show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination.
Subexponential logic is a variant of linear logic with a family of exponential connectives--called subexponentials--that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that classical propositional multiplicative linear logic extended with one unrestricted and two incomparable linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable.
This paper describes a quantum algorithm for proof search in sequent calculus of a subset of Linear Logic using the Grover Search Algorithm. We briefly overview the Grover Search Algorithm and Linear Logic, show the detailed steps of the algorithm and then present the results obtained on quantum simulators.
We show that it is coNP-complete to decide whether a given proof structure of pomset logic is a correct proof net, using the graph-theoretic used in a previous paper of ours (arXiv:1901.10247).
We show that for Multiplicative Exponential Linear Logic (without weakenings) the syntactical equivalence relation on proofs induced by cut-elimination coincides with the semantic equivalence relation on proofs induced by the multiset based relational model: one says that the interpretation in the model (or the semantics) is injective. We actually prove a stronger result: two cut-free proofs of the full multiplicative and exponential fragment of linear logic whose interpretations coincide in the multiset based relational model are the same "up to the connections between the doors of exponentia…
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑，其直观的片段。轻仿射逻辑有一个多项式成本削减消除（P时间正确性），并编码所有P时间图灵机（P时间完整性）。通过引入直觉轻仿射逻辑的证明网，证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面，P-Time正确性的证明描述了切割消除的复杂性是如何控制的，这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义，这是轻逻辑的一个特点。另一方面，P-时间完备性的证明，以及大量的编程实例，给出了一个非平凡的任务，编程资源的限制，使用直觉轻仿射逻辑推导程序的味道。
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
研究正确性与错误性变换程序逻辑，扩展以处理终止与非终止，证明其为自然关系语义的抽象解释，提供计算化方法设计可靠完备证明系统，并扩展 Hoare 逻辑及设计新前置条件逻辑。
Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of $λ$-calculus with parallelism and communication primitives, called $λ_{\unicode{8523}}$. We shall prove that $λ_{\unicode{8523}}$ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.
Topological Observations on Multiplicative Additive Linear Logic
作为一种尝试，以揭示的拓扑性质的组合策略的游戏语义，我们提出了一个“拓扑”的游戏乘加线性逻辑没有命题变量，包括削减移动。我们重铸的概念（获胜）的战略和削减消除在这种情况下的问题，并证明削减消除定理。最后，我们证明了可靠性和完备性。拓扑结构起着至关重要的作用，特别是通过策略形成一个层的事实。
We present a simple theory explaining the construction and the correctness of an incremental and worst-case optimal decision procedure for modal logic with eventualities. The procedure gives an abstract account of important aspects of Goré and Widmann's PDL prover. Starting from an input formula, the procedure grows a Pratt-style graph tableau until the tableau proves or disproves the satisfiability of the formula. The procedure provides a basis for practical provers since satisfiability and unsatisfiability of formulas can often be determined with small tableaux.
We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of {\em history-free} strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additive…
Logic Programming with Multiplicative Structures
本文研究纯乘法片段下基于证明网构造的逻辑编程框架，展示如何仅用资源保持且上下文无关的广义乘法操作实现上下文敏感方法，并证明部分方法超出线性逻辑MLL片段。
Type Isomorphisms for Multiplicative-Additive Linear Logic
本文研究了乘法-加法线性逻辑中的类型同构，通过扩展结果到完整MALL，揭示了分配律和消去律等更丰富的等式理论。
Total Outcome Logic: Unified Reasoning for a Taxonomy of Program Logics
本文提出总结果逻辑（TOL），一种统一逻辑，能表达部分与完全正确性等全部终止条件，扩展至非确定性与概率程序，并涵盖现有（不）正确性逻辑分类，实现统一推理。
We associate to every proof structure in multiplicative linear logic an ideal which represents the logical content of the proof as polynomial equations. We show how cut-elimination in multiplicative proof nets corresponds to instances of the Buchberger algorithm for computing Gröbner bases in elimination theory.
The original idea of proof nets can be formulated by means of interaction nets syntax. Additional machinery as switching, jumps and graph connectivity is needed in order to ensure correspondence between a proof structure and a correct proof in sequent calculus. In this paper we give an interpretation of proof nets in the syntax of string diagrams. Even though we lose standard proof equivalence, our construction allows to define a framework where soundness and well-typeness of a diagram can be verified in linear time.
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to capture computational effects) and monoidal (to reason about outcomes and reachability). OL expresses true positive bugs, while retaining correctness reasoning abilities as well. To formalize the applicabil…
A logical system derived from linear logic and called QMLL is introduced and shown able to capture all unitary quantum circuits. Conversely, any proof is shown to compute, through a concrete GoI interpretation, some quantum circuits. The system QMLL, which enjoys cut-elimination, is obtained by endowing multiplicative linear logic with a quantum modality.
The multiplicative fragment of Linear Logic is the formal system in this family with the best understood proof theory, and the categorical models which best capture this theory are the fully complete ones. We demonstrate how the Hyland-Tan double glueing construction produces such categories, either with or without units, when applied to any of a large family of degenerate models. This process explains as special cases a number of such models from the literature. In order to achieve this result, we develop a tensor calculus for compact closed categories with finite biproducts. We show how the …
A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of…
We present a new asynchronous model of computation named Stellar Resolution based on first-order unification. This model of computation is obtained as a formalisation of Girard's transcendental syntax programme, sketched in a series of three articles. As such, it is the first step towards a proper formal treatment of Girard's proposal to tackle first-order logic in a proofs-as-program approach. After establishing formal definitions and basic properties of stellar resolution, we explain how it generalises traditional models of computation, such as logic programming and combinatorial models such…
Given a logic presented in a sequent calculus, a natural question is that of equivalence of proofs: to determine whether two given proofs are equated by any denotational semantics, ie any categorical interpretation of the logic compatible with its cut-elimination procedure. This notion can usually be captured syntactically by a set of rule permutations. Very generally, proofnets can be defined as combinatorial objects which provide canonical representatives of equivalence classes of proofs. In particular, the existence of proof nets for a logic provides a solution to the equivalence problem of…
Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative $2$-dimensional syntax for multiplicative linear logic derivations. The syntax of string diagrams authorizes the definition of a framework where the sequentializability of a term, i.e. deciding whether the term corresponds to a correct derivation, can be verified in linear time. Furthermore, we can use this syntax to define a denotational semantics for multiplica…
An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets
本文研究MLL证明网并行消去的组合性质，通过路径约束保证无限加权和归约的有限性，并证明该约束适用于MELL泰勒展开中的微分网，为线性逻辑定量语义提供充分条件。
Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered. An element of the relational interpretation of a proof-structure R with conclusion $Γ$ acts thus as a type (refining $Γ$) having R as an inhabitant. We are interested in the following type-checking question: given a proof-structure R, a list of formulae $Γ$, and a point x in the relational interpretation of $Γ$, is x in the interpretation of R? This question is decidable. We present here an algorithm that decides it …
Kozen and Tiuryn have introduced the substructural logic $\mathsf{S}$ for reasoning about correctness of while programs (ACM TOCL, 2003). The logic $\mathsf{S}$ distinguishes between tests and partial correctness assertions, representing the latter by special implicational formulas. Kozen and Tiuryn's logic extends Kleene altebra with tests, where partial correctness assertions are represented by equations, not terms. Kleene algebra with codomain, $\mathsf{KAC}$, is a one-sorted alternative to Kleene algebra with tests that expands Kleene algebra with an operator that allows to construct a Boo…
This special issue cover the seventh and last conference of the CL&C series, started in 2006 in San Servolo. Topics are the computational content of logics between intuitionistic logic and classical logic, through normalization, and a new topic, cyclic proofs and the complexity of checking the correctness of a cyclic proof. Accepted papers include an empirical comparison of time consumption of different normalization algorithms, and new reductions sets for several extensions of intuitionistic logic having the Herbrand disjunction property. Another paper provides a reduction set for admissible …
We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method which should be well known but is often neglected. Also, we show how to prove completeness and correctness in the presence of SLD-tree pruning, and point out that approximate specifications simplify specifications and proofs. We compare the proof methods to declarative diagnosis (algorithmic debugging), showing that approximate specifications eliminate a major drawback of the latter. We argue that our proof methods ref…
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
A Real-Valued Modal Logic
本文提出一种实值多值模态逻辑，结合Kripke语义与实数上的格群运算，通过带标签tableau系统获得coNEXPTIME上界，并建立模态-乘法片段的消割sequent演算及扩展阿贝尔逻辑的完备性。
Modelling Multiplicative Linear Logic via Deep Inference
本文研究乘法线性逻辑中深推理系统与标准矢列演算之间的翻译关系，提出简化翻译并证明标准建模方法对翻译保持不变，同时给出一个文献中缺失的关于 par 与 tensor 数量的可证性必要条件。
On the role of connectivity in Linear Logic proofs
本文研究了线性逻辑证明中连通性的作用，提出了一种几何条件将必要性质转化为充分条件，从而为线性逻辑的片段提供正确性标准。
We present the stellar resolution, a "flexible" tile system based on Robinson's first-order resolution. After establishing formal definitions and basic properties of the stellar resolution, we show its Turing-completeness and to illustrate the model, we exhibit how it naturally represents computation with Horn clauses and automata as well as nondeterministic tiling constructions used in DNA computing. In the second and main part, by using the stellar resolution, we formalise and extend ideas of a new alternative to proof-net theory sketched by Girard in his transcendental syntax programme. In …
Using Z3 to Verify Inferences in Fragments of Linear Logic
本文提出一种基于Z3定理证明器的Gentzen风格线性逻辑矢列式模板，用于自动验证推理规则，并在MLL+Mix和MILL两个片段上验证了若干导出推理规则。
Computational Logic is the use of computers to establish facts in a logical formalism. Originating in 19th-century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the "LCF approach" pioneered by Robin Milner FRS, where proofs can be constructed interactively or with the help of users' code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger…
The syntactic calculus of Lambek is a deductive system for the multiplicative fragment of intuitionistic non-commutative linear logic. As a fine-grained calculus of resources, it has many applications, mostly in formal computational investigations of natural languages. This paper introduces a calculus of beta-eta-long normal forms for derivations in the Lambek calculus with multiplicative unit and conjunction among its logical connectives. Reduction to normal form follows the normalization by evaluation (NbE) strategy: (i) evaluate a derivation in a Kripke model of Lambek calculus; (ii) extrac…
Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the…
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
本文提出结果分离逻辑（OSL），一种同时支持正确性与不正确性推理的程序逻辑，通过框架规则和新的三归结符号执行算法，实现对具有计算效应程序的局部推理，推进了分离逻辑的合成性。
Partial Incorrectness Logic
本文提出部分不正确性逻辑，以 Dijkstra 式谓词转换器刻画“允许不可达”，并阐明其与完全不正确性逻辑及部分/完全正确性的对偶关系。
This paper establishes the normalisation of natural deduction or lambda calculus formulation of Intuitionistic Non Commutative Logic --- which involves both commutative and non commutative connectives. This calculus first introduced by de Groote and as opposed to the classical version by Abrusci and Ruet admits a full entropy which allow order to be relaxed into any suborder. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Regarding Intuitionistic Non Commutative Logic with full entrop…
Nowadays, numerous services based on large-scale distributed systems have been developed to boost the convenience of human life. On the other side, it becomes a significant challenge to ensure the correctness and properties of these systems due to the complex and nested architecture. Although concurrent separation logic (CSL) has partially tackled the problem by specifying systems and verifying the correctness of them, it faces modularity issues. In this paper, we propose an extended concurrent separation logic (ECSL) to address the modularity issues of CSL with the support of the temporal ext…
Proving correctness of Timed Concurrent Constraint Programs
提出了一种用于时间并发约束程序正确性推理的时态逻辑。这种逻辑是基于模态，它允许人们指定一个过程产生什么作为对其环境输入的反应。这些模态提供了一个假设/承诺风格的规范，允许一个健全的和完整的组合公理化的反应行为的定时并发约束程序。
Technically speaking, the transcendental syntax is about designing logics with a computational foundation. It suggests a new framework for proof theory where logic (proofs, formulas, truth, ...) is no more primitive but computation is. All the logical entities and activities will be presented as formatting/structuring on a given model of computation which should be as general, simple and natural as possible. The selected ground for logic in the transcendental syntax is a model of computation I call "stellar resolution" which is basically a logic-free reformulation of Robinson's first-order cla…
We show that a proof in multiplicative linear logic can be represented as a decorated surface, such that two proofs are logically equivalent just when their surfaces are geometrically equivalent. This is an extended abstract for arXiv:1601.05372.
In this work we investigate how to extract alternating time bounds from 'focussed' proof systems. Our main result is the obtention of fragments of MALLw (MALL with weakening) complete for each level of the polynomial hierarchy. In one direction we encode QBF satisfiability and in the other we encode focussed proof search, and we show that the composition of the two encodings preserves quantifier alternation, yielding the required result. By carefully composing with well-known embeddings of MALLw into MALL, we obtain a similar delineation of MALL formulas, again carving out fragments complete f…
Technical Report: Distribution Temporal Logic: Combining Correctness with Quality of Estimation
本文提出分布时间逻辑（DTL），用于描述部分可观测系统中涉及不确定性和可能性的属性，提供了一种安全的公式化方法及监控算法，并通过救援机器人应用案例验证。
Linear Realisability over nets: multiplicatives (long version)
针对线性逻辑乘法片段，提出基于正交性的新可实现性模型，定义广义公理的截消，证明其对MLL*和MLL的适当性与完备性，解决广义公理下的可实现性建模问题。
Model Checking Logical Actions in Magic Tricks
本文提出魔术模型检测（MTMC）技术，将纸牌魔术的逻辑正确性问题归约为模型检测问题，以验证魔术设计是否符合预期。
Resource-distribution via Boolean constraints
我们考虑的问题，搜索证明顺序表示逻辑与乘法（或内涵）连接词。具体来说，我们从线性逻辑的乘法片段开始，一方面扩展到线性逻辑及其添加剂，另一方面扩展到集束蕴涵逻辑BI的添加剂。我们给出了一个代数方法计算乘法规则中的侧公式的分布，一旦有足够的信息，它允许在证明的分支上确定公式的发生或不发生。这样一个规则的结论中的每个公式都被赋予一个布尔表达式。随着搜索的进行，生成一组布尔约束方程。我们表明，这样一组方程的解决方案确定了相应的证明给定的搜索。我们解释了一系列的战略，从懒惰的渴望，解决约束方程组。我们指出如何将我们的方法系统地应用到大家庭的相关系统。
A Proof-theoretic Semantics for Intuitionistic Linear Logic
本文扩展了Gheorghiu等人对直觉主义乘法线性逻辑的基扩展语义，为完整的直觉主义线性逻辑（包括模态连接词bang）提供了证明论语义，并讨论了处理bang连接词的挑战。
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further …
Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic
研究扩展线性逻辑证明结构正确性标准的性质，提出对证明结构的几何限制使其成为充分性质，引入VMELL片段，将!演算项翻译为证明网，分解λ演算翻译，证明消去切割模拟!归约并给出!演算项的证明网特征。
Local Completeness Logic (LCL) has been put forward as a program logic for proving both the correctness and incorrectness of program specifications. LCL is an abstract logic, parameterized by an abstract domain that allows combining over- and under-approximations of program behaviors. It turns out that LCL instantiated to the trivial singleton abstraction boils down to O'Hearn incorrectness logic, which allows us to prove the presence of program bugs. It has been recently proved that suitable extensions of Kleene algebra with tests (KAT) allow representing both O'Hearn incorrectness and Hoare …
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.
Modules and Logic Programming
我们研究的条件下，同时建设的证明网的框架开发的Andreoli在最近的论文。为此，我们定义了特定的正确性标准。我们首先研究封闭的模块（即有效性的执行一个逻辑程序），然后扩展该标准的开放模块（即有效性在执行过程中）区分标准的非循环性和可连接性，以允许增量验证。
On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
本文提出首个带while循环的相对完备的基于满足性的量子霍尔逻辑，通过构造最弱前置项演算证明完备性，并成功验证Deutsch算法和量子隐形传态的正确性。
Introduction to linear logic and ludics, part II
本文是《线性逻辑和态极逻辑引论》一文的第二部分。它致力于证明网络，在有限的，但中心，框架的乘法线性逻辑和ludics，这是最近发展的目的是进一步揭示基本的互动性质的计算和逻辑。我们希望本文能对这一新的理论带来一些计算机科学方面的启示。
A non-commutative, non-associative weakening of Girard's linear logic is developed for multiplicative and additive connectives. Additional assumptions capture the logic of quantic measurements.
We present Classical BI (CBI), a new addition to the family of bunched logics which originates in O'Hearn and Pym's logic of bunched implications BI. CBI differs from existing bunched logics in that its multiplicative connectives behave classically rather than intuitionistically (including in particular a multiplicative version of classical negation). At the semantic level, CBI-formulas have the normal bunched logic reading as declarative statements about resources, but its resource models necessarily feature more structure than those for other bunched logics; principally, they satisfy the req…
Phase Semantic Cut-elimination for Intuitionistic Linear Logic with Least and Greatest Fixed Points
研究具有最小和最大不动点的直觉主义命题乘加线性逻辑（$\mu$IMALL）的消去切割定理，通过定义相位语义，证明其可靠性与无切割完全性，改进前人论证方法来达成该定理的证明。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。