the proceedings contain 95 papers. the topics discussed include: towards a more efficient approach for the satisfiability of two-variable logic;demonic lattices and semilattices in relational semigroups with ordinary ...
ISBN:
(纸本)9781665448956
the proceedings contain 95 papers. the topics discussed include: towards a more efficient approach for the satisfiability of two-variable logic;demonic lattices and semilattices in relational semigroups with ordinary composition;on logics and homomorphism closure;universal Skolem sets;evidenced frames: a unifying framework broadening realizability models;behavioral preorders via graded monads;the undecidability of system F typability and type checking for reductionists;complexity lower bounds from algorithm design;on the logical structure of choice and bar induction principles;compositional relational reasoning via operational game semantics;continuous one-counter automata;and in search of lost time: axiomatizing parallel composition in process algebras.
Graph neural networks (GNNs) are deep learning architectures for machine learning problems on graphs. It has recently been shown that the expressiveness of GNNs can be characterised precisely by the combinatorial Weis...
详细信息
ISBN:
(纸本)9781665448956
Graph neural networks (GNNs) are deep learning architectures for machine learning problems on graphs. It has recently been shown that the expressiveness of GNNs can be characterised precisely by the combinatorial Weisfeiler-Leman algorithms and by finite variable counting logics. the correspondence has even led to new, higher-order GNNs corresponding to the WL algorithm in higher dimensions. the purpose of this paper is to explain these descriptive characterisations of GNNs.
We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is an FO-definable language that is monotone in monadic predicates but not definab...
详细信息
ISBN:
(纸本)9781665448956
We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is an FO-definable language that is monotone in monadic predicates but not definable in FO+. this provides a simple proof that Lyndon's preservation theorem fails on finite structures. We additionally show that given a regular language, it is undecidable whether it is definable in FO+.
In this paper we consider the relationship between monomial-size and bit-complexity in Sums-of-Squares (SOS) in Polynomial Calculus Resolution over rationals (PCR/Q). We show that there is a set of polynomial constrai...
详细信息
ISBN:
(纸本)9781665448956
In this paper we consider the relationship between monomial-size and bit-complexity in Sums-of-Squares (SOS) in Polynomial Calculus Resolution over rationals (PCR/Q). We show that there is a set of polynomial constraints Q(n) over Boolean variables that has both SOS and PCR/Q refutations of degree 2 and thus with only polynomially many monomials, but for which any SOS or PCR/Q refutation must have exponential bit-complexity, when the rational coefficients are represented withtheir reduced fractions written in binary.
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. these two semantic approaches build on previous work that used an explicit source of randomness to reason about h...
详细信息
ISBN:
(纸本)9781665448956
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. these two semantic approaches build on previous work that used an explicit source of randomness to reason about higher-order probabilistic programs.
In the search for a logic capturing polynomial time the most promising candidates are Choiceless Polynomial Time (CPT) and rank logic. Rank logic extends fixed-point logic with counting by a rank operator over prime f...
详细信息
ISBN:
(纸本)9781665448956
In the search for a logic capturing polynomial time the most promising candidates are Choiceless Polynomial Time (CPT) and rank logic. Rank logic extends fixed-point logic with counting by a rank operator over prime fields. We show that the isomorphism problem for CFI graphs over Z(2i) cannot be defined in rank logic, even if the base graph is totally ordered. However, CPT can define this isomorphism problem. We thereby separate rank logic from CPT and in particular from polynomial time.
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense o...
详细信息
ISBN:
(纸本)9781665448956
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of beta/eta-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic ...
详细信息
ISBN:
(纸本)9781665448956
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of infinity-groupoid internal to type theory and we prove that the type of such infinity-groupoids is equivalent to the universe of types. that is, every type admits the structure of an infinity-groupoid internally, and this structure is unique.
We study the extent to which it is possible to approximate the optimal value of a Unique Games instance in Fixed-Point logic with Counting (FPC). We prove two new FPC-inexpressibility results for Unique Games: the exi...
详细信息
ISBN:
(纸本)9781665448956
We study the extent to which it is possible to approximate the optimal value of a Unique Games instance in Fixed-Point logic with Counting (FPC). We prove two new FPC-inexpressibility results for Unique Games: the existence of a ( 1/2, 1/3 I delta)-inapproximability gap, and inapproximability to within any constant factor. Previous recent work has established similar FPC-inapproximability results for a small handful of other problems. Our construction builds upon some of these ideas, but contains a novel technique. While most FPC-inexpressibility results are based on variants of the CFI-construction, ours is significantly different.
We study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositi...
详细信息
ISBN:
(纸本)9781665448956
We study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositions must be constructive in some sense, whereas proofs of classical propositions proceed by contradiction. the system, in natural deduction style, is shown to be sound and complete with respect to a Kripke semantics. We develop the system from the perspective of the propositions-as-types correspondence by deriving a term assignment system with confluent reduction. the proof of strong normalization relies on a translation to System F with Mendler-style recursion.
暂无评论