the proceedings contain 72 papers. the topics discussed include: complete game logic with sabotage;an expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications;non-elem...
ISBN:
(纸本)9798400706608
the proceedings contain 72 papers. the topics discussed include: complete game logic with sabotage;an expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications;non-elementary compression of first-order proofs in deep inference using epsilon-terms;verifying unboundedness via amalgamation;genericity through stratification;deterministic sub-exponential algorithm for discounted-sum games with unary weights;decidability and complexity of decision problems for affine continuous VASS;injective hardness condition for PCSPs;on the decidability of monadic second-order logic with arithmetic predicates;element-free probability distributions and random partitions;the complexity of resilience problems via valued constraint satisfaction problems;and discounted-sum automata with real-valued discount factors.
the proceedings contain 64 papers. the topics discussed include: transducers of polynomial growth;normalization for multimodal type theory;computing the density of the positivity set for linear recurrence sequences;qu...
ISBN:
(纸本)9781450393515
the proceedings contain 64 papers. the topics discussed include: transducers of polynomial growth;normalization for multimodal type theory;computing the density of the positivity set for linear recurrence sequences;quantum weakest preconditions for reasoning about expected runtimes of quantum programs;on the Skolem problem and the Skolem conjecture;on the satisfiability of context-free string constraints with subword-ordering;identity testing for radical expressions;varieties of quantitative algebras and their monads;quantum expectation transformers for cost analysis;solvability of orbit-finite systems of linear equations;semantics for two-dimensional type theory;and the amazing mixed polynomial closure and its applications to two-variable first-order logic.
the proceedings contain 73 papers. the topics discussed include: a tale of intersection types;automatic structures: twenty years later;logic beyond formulas: a proof system on graphs;a higher structure identity princi...
ISBN:
(纸本)9781450371049
the proceedings contain 73 papers. the topics discussed include: a tale of intersection types;automatic structures: twenty years later;logic beyond formulas: a proof system on graphs;a higher structure identity principle;the integers as a higher inductive type;space-efficient query evaluation over probabilistic event streams;algebraic models of simple type theories: a polynomial approach;approximating values of generalized-reachability stochastic games;reconciling noninterference and gradual typing;deciding differential privacy for programs with finite inputs and outputs;universal equivalence and majority of probabilistic programs over finite fields;and modal logics with composition on finite forests: expressivity and complexity.
the proceedings contain 67 papers. the topics discussed include: commutativity in automated verification;applications of information inequalities to database theory problems;a system of inference based on proof search...
ISBN:
(纸本)9798350335873
the proceedings contain 67 papers. the topics discussed include: commutativity in automated verification;applications of information inequalities to database theory problems;a system of inference based on proof search: an extended abstract;the descriptive complexity of graph neural networks;simulating logspace-recursion with logarithmic quantifier depth;embedded finite models beyond restricted quantifier collapse;distal combinatorial tools for graphs of bounded twin-width;a categorical account of composition methods in logic;the logic of prefixes and suffixes is elementary under homogeneity;revisiting membership problems in subclasses of rational relations;verifying linear temporal specifications of constant-rate multi-mode systems;and a higher-order indistinguishability logic for cryptographic reasoning.
the proceedings contain 62 papers. the topics discussed include: separation and covering for group based concatenation hierarchies;why propositional quantification makes modal logics on trees robustly hard?;higher-kin...
ISBN:
(纸本)9781728136080
the proceedings contain 62 papers. the topics discussed include: separation and covering for group based concatenation hierarchies;why propositional quantification makes modal logics on trees robustly hard?;higher-kinded data types: syntax and semantics;model comparison games for horn description logics;the logic of action lattices is undecidable;point-width and max-CSPs;path spaces of higher inductive types in homotopy type theory;perspective games;the geometry of Bayesian programming;categorical semantics for time travel;backprop as functor: a compositional perspective on supervised learning;descriptive complexity for minimal time of cellular automata;a sequent calculus for opetopes;and approximate span liftings: compositional semantics for relaxations of differential privacy.
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.
Since the introduction of the semilattice relevant logic S by [Urquhart 1972, 1973], its decision problem has persisted as an open problem. [Urquhart 1984] showed that many relevant logics are undecidable, yet S elude...
详细信息
ISBN:
(纸本)9798400706608
Since the introduction of the semilattice relevant logic S by [Urquhart 1972, 1973], its decision problem has persisted as an open problem. [Urquhart 1984] showed that many relevant logics are undecidable, yet S eluded these techniques. Eventually, this led experts, including [Urquhart 2016], to conjecture that S is decidable. Contrary to this conjecture, by interpreting a tiling problem, we show that S is undecidable.
We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. th...
详细信息
ISBN:
(纸本)9798400706608
We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. the axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories.
We propose to study transformations on graphs, and more generally structures, by looking at how the cut-rank (as introduced by Oum) of subsets is affected when going from the input structure to the output structure. W...
详细信息
ISBN:
(纸本)9798400706608
We propose to study transformations on graphs, and more generally structures, by looking at how the cut-rank (as introduced by Oum) of subsets is affected when going from the input structure to the output structure. We consider transformations in which the underlying sets are the same for boththe input and output, and so the cut-ranks of subsets can be easily compared. the purpose of this paper is to give a characterisation of logically defined transductions that is expressed in purely structural terms, without referring to logic: transformations which decrease the cut-rank, in the asymptotic sense, are exactly those that can be defined in monadic second-order logic. this characterisation assumes that the transduction has inputs of bounded treewidth;we also show that the characterisation fails in the absence of any assumptions.
Game logic with sabotage (GLs) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. GLs can be used to mode...
详细信息
ISBN:
(纸本)9798400706608
Game logic with sabotage (GLs) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. GLs can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to game logic, which is strictly less expressive, GLs is exactly as expressive as the modal mu-calculus. this reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games. A natural Hilbert-style proof calculus for GLs is presented and proved complete using syntactic equiexpressiveness reductions. the completeness of a simple extension of Parikh's calculus for game logic follows.
暂无评论