TOCL 欢迎与计算机科学主题相关的逻辑各个方面的提交。该领域在计算机科学方面有着悠久的传统。获得 ACM 图灵奖的几位研究人员也为该领域做出了贡献，即 EDGAR CODD（关系数据库系统）、STEPHEN COOK（逻辑理论的复杂性）、EDSGER W. DIJKSTRA、ROBERT W. FLOYD、TONY HOARE、AMIR PNUELI、DANA SCOTT、EDMOND M. CLARKE、ALLEN E. EMERSON 和 JOSEPH SIFAKIS（程序逻辑、程序推导和验证、编程语言语义）、ROBIN MILNER（交互式定理证明、并发演算和函数式编程）和 JOHN MCCARTHY（函数式编程和人工智能中的逻辑）。逻辑在计算机科学中继续发挥重要作用，并已渗透到其多个领域，包括人工智能、计算复杂性、数据库系统和编程语言。本刊编委会寻求并希望吸引高- 在上述所有计算逻辑领域提交高质量的论文，使 TOCL 成为该领域的标准参考。理论和应用论文重新寻找。特别欢迎提交展示逻辑在计算机科学中的新颖使用的提交。

ACM Transactions on Computational Logic welcomes submissions on all aspects of logic related to computer science. This field has a long-standing tradition within computer science, with several Turing Award winners contributing significantly, including EDGAR CODD (relational database systems), STEPHEN COOK (complexity of logical theories), EDSGER W. DIJKSTRA, ROBERT W. FLOYD, TONY HOARE, AMIR PNUELI, DANA SCOTT, EDMOND M. CLARKE, ALLEN E. EMERSON, and JOSEPH SIFAKIS (program logic, program derivation and verification, semantics of programming languages), ROBIN MILNER (interactive theorem proving, concurrent calculi, and functional programming), and JOHN MCCARTHY (logic in functional programming and artificial intelligence). Logic continues to play a vital role in computer science and has permeated various fields, including artificial intelligence, computational complexity, database systems, and programming languages. The editorial board seeks to attract high-quality submissions in all areas of computational logic, aiming to make ACM Transactions on Computational Logic a standard reference in the field. We particularly welcome submissions that showcase novel uses of logic in computer science.

《ACM Transactions on Computational Logic》欢迎与计算机科学相关的逻辑各个方面的投稿。该领域在计算机科学中有着悠久的传统，许多获得ACM图灵奖的研究人员对其做出了重要贡献，包括EDGAR CODD（关系数据库系统）、STEPHEN COOK（逻辑理论的复杂性）、EDSGER W. DIJKSTRA、ROBERT W. FLOYD、TONY HOARE、AMIR PNUELI、DANA SCOTT、EDMOND M. CLARKE、ALLEN E. EMERSON和JOSEPH SIFAKIS（程序逻辑、程序推导和验证、编程语言语义）、ROBIN MILNER（交互式定理证明、并发演算和函数式编程）以及JOHN MCCARTHY（函数式编程和人工智能中的逻辑）。逻辑在计算机科学中继续发挥着重要作用，并已渗透到多个领域，包括人工智能、计算复杂性、数据库系统和编程语言。本刊编委会希望吸引在上述所有计算逻辑领域提交高质量论文，使《ACM Transactions on Computational Logic》成为该领域的标准参考。我们欢迎理论和应用论文的投稿，特别是那些展示逻辑在计算机科学中新颖应用的研究。

ACM Transactions on Computational Logic

We prove new upper and lower bounds on the number of iterations the \(k\) -dimensional Weisfeiler-Leman algorithm ( \(k\) -WL) requires until stabilization. For \(k\geq 3\) , we show that \(k\) -WL stabilizes after at most \(O(kn^{k-1}\log n)\) iterations (where \(n\) denotes the number of vertices of the input structures), obtaining the first improvement over the trivial upper bound of \(n^{k}-1\) and extending a previous upper bound of \(O(n\log n)\) for \(k=2\) [Lichter et al., LICS 2019]. We complement our upper bounds by constructing \(k\) -ary relational structures on which \(k\) -WL requires at least \(n^{\Omega(k)}\) iterations to stabilize. This improves over a previous lower bound of \(n^{\Omega(k/\log k)}\) [Berkholz, Nordström, LICS 2016]. We also investigate tradeoffs between the dimension and the iteration number of WL, and show that \(d\) -WL, where \(d=\lceil\frac{3(k+1)}{2}\rceil\) , can simulate the \(k\) -WL algorithm using only \(O(k^{2}\cdot n^{\lfloor k/2\rfloor+1}\log n)\) many iterations, but still requires at least \(n^{\Omega(k)}\) iterations for any \(d\) (that is sufficiently smaller than \(n\) ). The number of iterations required by \(k\) -WL to distinguish two structures corresponds to the quantifier rank of a sentence distinguishing them in the \((k+1)\) -variable fragment \(\mathsf{C}_{k+1}\) of first-order logic with counting quantifiers. Hence, our results also imply new upper and lower bounds on the quantifier rank required in the logic \(\mathsf{C}_{k+1}\) , as well as tradeoffs between variable number and quantifier rank.

Martin Grohe

Moritz Lichter

Daniel Neuen

The Iteration Number of the Weisfeiler-Leman Algorithm

Weisfeiler-Leman算法的迭代次数

We introduce a subclass of concurrent game structures (CGS) with imperfect information in which agents are endowed with private data-sharing capabilities. Importantly, our CGSs are such that it is still decidable to model-check these CGSs against a relevant fragment of ATL. These systems can be thought as a generalisation of architectures allowing information forks, that is, cases where strategic abilities lead to certain agents outside a coalition privately sharing information with selected agents inside that coalition. Moreover, in our case, in the initial states of the system, we allow information forks from agents outside a given set \(A\) to agents inside this group \(A\) . For this reason, together with the fact that the communication in our models underpins a specialised form of broadcast, we call our formalism \(A\) -cast systems . To underline, the fragment of ATL for which we show the model-checking problem to be decidable over \(A\) -cast is a large and significant one; it expresses coalitions over agents in any subset of the set \(A\) . Indeed, as we show, our systems and this ATL fragments can encode security problems that are notoriously hard to express faithfully: terrorist-fraud attacks in identity schemes.

Francesco Belardinelli

Ioana Boureanu

Catalin Dima

Vadim Malvone

Model Checking Strategic Abilities in Information-sharing Systems

信息共享系统中的策略能力模型检测

Higher-order unification has been shown to be undecidable [Huet 1973]. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has most general unifiers [1991]. We extend the algorithm to higher-order rational terms (a.k.a. regular Böhm trees [Huet 1998], a form of cyclic \(\lambda\) -terms) and show that pattern unification on higher-order rational terms is decidable and has most general unifiers. We prove the soundness and completeness of the algorithm.

Zhibo Chen

Frank Pfenning

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns

基于饱和的高阶有理模式统一算法

We prove that the combinatorial Weisfeiler-Leman algorithm of dimension (3 k +4) is a complete isomorphism test for the class of all graphs of rank width at most k . Rank width is a graph invariant that, similarly to tree width, measures the width of a certain style of hierarchical decomposition of graphs; it is equivalent to clique width. It was known that isomorphism of graphs of rank width k is decidable in polynomial time (Grohe and Schweitzer, FOCS 2015), but the best previously known algorithm has a running time n f(k) for a non-elementary function f . Our result yields an isomorphism test for graphs of rank width k running in time n O(k) . Another consequence of our result is the first polynomial-time canonisation algorithm for graphs of bounded rank width. Our second main result is that fixed-point logic with counting captures polynomial time on all graph classes of bounded rank width.

Canonisation and Definability for Graphs of Bounded Rank Width

有界秩宽图的规范化和可定义性

We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity. Properness (i.e., closure under uniform substitution of all parametric parts in rules) is the main technical novelty of the present proposal, allowing both for the smoothest proof of cut elimination and for the development of an overarching and modular treatment for a vast class of axiomatic extensions and expansions of intuitionistic, bi-intuitionistic, and classical linear logics with exponentials. Our proposal builds on an algebraic and order-theoretic analysis of linear logic and applies the guidelines of the multi-type methodology in the design of display calculi.

Giuseppe Greco

Alessandra Palmigiano

Linear Logic Properly Displayed

线性逻辑的恰当展示

We give a complete complexity classification for the problem of finding a solution to a given system of equations over a fixed finite monoid, given that a solution over a more restricted monoid exists. As a corollary, we obtain a complexity classification for the same problem over groups.

Alberto Larrauri

Stanislav Živný

Solving promise equations over monoids and groups

求解幺半群和群上的承诺方程

We introduce a novel model-theoretic framework inspired from graph modification and based on the interplay between model theory and algorithmic graph minors. The core of our framework is a new compound logic operating with two types of sentences, expressing graph modification: the modulator sentence, defining some property of the modified part of the graph, and the target sentence, defining some property of the resulting graph. In our framework, modulator sentences are in counting monadic second-order logic ( CMSO ) and have models of bounded treewidth, while target sentences express first-order logic ( FO ) properties. Our logic captures problems that are not definable in first-order logic and, moreover, may have instances of unbounded treewidth. Our main result is that, for this compound logic, model-checking can be done in quadratic time on minor-free graphs. The proposed logic can be seen as a general framework to capitalize on the potential of the irrelevant vertex technique. It gives a way to deal with problem instances of unbounded treewidth, for which Courcelle's theorem does not apply. The proof of our meta-theorem combines novel combinatorial results related to the Flat Wall theorem along with elements of the proof of Courcelle's theorem and Gaifman's theorem. Our algorithmic meta-theorem encompasses, unifies, and extends the known meta-algorithmic results for CMSO and FO on minor-closed graph classes.

Abbreviation	ACM Trans. Comput. Logic
Journal Impact	0.67
Quartiles(Global)	LOGIC(Q1)

ISSN	1529-3785, 1557-945X
h-index	52

Publication Information	Publisher: Association for Computing Machinery (ACM)，Publishing cycle: Quarterly，Journal Type: journal，Open Access Journals: No
Basic data	Year of publication: 2000，Proportion of original research papers: 100.00%，Self Citation Rate:14.30%， Gold OA Rate: 3.41%
Average review cycle	网友分享经验：>12周，或约稿
Average recruitment ratio	网友分享经验：容易

ACM Transactions on Computational Logic

Journal Citation Format

A journal article with 1 author

A journal article with 2 authors

A journal article with 3 authors

A journal article with 5 or more authors

Books Citation Format

Thesis Citation Format

Web sites Citation Format

Patent Citation Format

Staying up late manually editing references? ivySCI automatically matches journals and helps you generate references with a single click.

Share Submission Experience

The Iteration Number of the Weisfeiler-Leman Algorithm

Model Checking Strategic Abilities in Information-sharing Systems

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns

Canonisation and Definability for Graphs of Bounded Rank Width

Linear Logic Properly Displayed

The Iteration Number of the Weisfeiler-Leman Algorithm

Model Checking Strategic Abilities in Information-sharing Systems

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns

Solving promise equations over monoids and groups

Compound Logics for Modification Problems