189 Search Results for "Silva, Alexandra"


Volume

LIPIcs, Volume 288

32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

CSL 2024, February 19-23, 2024, Naples, Italy

Editors: Aniello Murano and Alexandra Silva

Volume

LIPIcs, Volume 241

47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

MFCS 2022, August 22-26, 2022, Vienna, Austria

Editors: Stefan Szeider, Robert Ganian, and Alexandra Silva

Volume

LIPIcs, Volume 211

9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

CALCO 2021, August 31 to September 3, 2021, Salzburg, Austria

Editors: Fabio Gadducci and Alexandra Silva

Document
Complete Volume
LIPIcs, Volume 288, CSL 2024, Complete Volume

Authors: Aniello Murano and Alexandra Silva

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
LIPIcs, Volume 288, CSL 2024, Complete Volume

Cite as

32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 1-892, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Proceedings{murano_et_al:LIPIcs.CSL.2024,
  title =	{{LIPIcs, Volume 288, CSL 2024, Complete Volume}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{1--892},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024},
  URN =		{urn:nbn:de:0030-drops-196423},
  doi =		{10.4230/LIPIcs.CSL.2024},
  annote =	{Keywords: LIPIcs, Volume 288, CSL 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Aniello Murano and Alexandra Silva

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{murano_et_al:LIPIcs.CSL.2024.0,
  author =	{Murano, Aniello and Silva, Alexandra},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.0},
  URN =		{urn:nbn:de:0030-drops-196436},
  doi =		{10.4230/LIPIcs.CSL.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Ackermann Award
The Ackermann Award 2023

Authors: Maribel Fernández, Jean Goubault-Larrecq, and Delia Kesner

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
Report on the 2023 Ackermann Award.

Cite as

Maribel Fernández, Jean Goubault-Larrecq, and Delia Kesner. The Ackermann Award 2023. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{fernandez_et_al:LIPIcs.CSL.2024.1,
  author =	{Fern\'{a}ndez, Maribel and Goubault-Larrecq, Jean and Kesner, Delia},
  title =	{{The Ackermann Award 2023}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{1:1--1:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.1},
  URN =		{urn:nbn:de:0030-drops-196446},
  doi =		{10.4230/LIPIcs.CSL.2024.1},
  annote =	{Keywords: lambda-calculus, computational complexity, geometry of interaction, abstract machines, intersection types}
}
Document
Invited Talk
Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk)

Authors: Balder ten Cate

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
The Craig Interpolation Property (CIP) is a property of logics. It states that, for all formulas φ and ψ, if φ ⊧ ψ, then there exists an "interpolant" ϑ such that φ ⊧ ϑ and ϑ ⊧ ψ, and such that all non-logical symbols occurring in ϑ occur both in φ and in ψ. Craig [Craig, 1957] proved in 1957 that first-order logic (FO) has this property. Since then, many refinements of Craig’s result have been obtained (e.g., [Otto, 2000; Benedikt et al., 2016]). These have found applications in various areas of computer science and AI, including formal verification, modular hard/software specification and automated deduction [McMillan, 2018; Calvanese et al., 2020; Hoder et al., 2012], and more recently prominently in databases [Toman and Weddell, 2011; Benedikt et al., 2016] and knowledge representation [Lutz and Wolter, 2011; ten Cate et al., 2013; Koopmann and Schmidt, 2015]. In this invited talk, we will survey recent work pertaining to Craig interpolation for various important decidable fragment of first-order logic, including guarded fragments, finite-variable fragments, and ordered fragments. Most of these fragments lack the CIP (the guarded-negation fragment GNFO being a notable exception [Bárány et al., 2013]). We will discuss strategies that have been proposed in recent literature to deal with this lack of CIP, as well as recent results that shed light on where, within the landscape of decidable fragment of first-order logic, one may find logics that enjoy CIP [Jung and Wolter, 2021; ten Cate and Comer, 2023].

Cite as

Balder ten Cate. Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{tencate:LIPIcs.CSL.2024.2,
  author =	{ten Cate, Balder},
  title =	{{Craig Interpolation for Decidable Fragments of First-Order Logic}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.2},
  URN =		{urn:nbn:de:0030-drops-196488},
  doi =		{10.4230/LIPIcs.CSL.2024.2},
  annote =	{Keywords: First-Order Logic, Decidable Fragments, Craig Interpolation}
}
Document
Invited Talk
Artificial Intelligence and Artificial Ignorance (Invited Talk)

Authors: Georg Gottlob

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
This invited talk first delves into the division between the two primary branches of AI research: symbolic AI, which predominantly focuses on knowledge representation and logical reasoning, and sub-symbolic AI, primarily centered on machine learning employing neural networks. We explore both the notable accomplishments and the challenges encountered in each of these approaches. We provide instances where traditional deep learning encounters limitations, and we elucidate significant obstacles in achieving automated symbolic reasoning. We then discuss the recent groundbreaking advancements in generative AI, driven by language models such as ChatGPT. We showcase instances where these models excel and, conversely, where they exhibit shortcomings and produce erroneous information. We identify and illustrate five key reasons for potential failures in language models, which include: [(i)] 1) information loss due to data compression, 2) training bias, 3) the incorporation of incorrect external data, 4) the misordering of results, and 5) the failure to detect and resolve logical inconsistencies contained in a sequence of LLM-generated prompt-answers. Lastly, we touch upon the Chat2Data project, which endeavors to leverage language models for the automated verification and enhancement of relational databases, all while mitigating the pitfalls (i)-(v) mentioned earlier.

Cite as

Georg Gottlob. Artificial Intelligence and Artificial Ignorance (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{gottlob:LIPIcs.CSL.2024.3,
  author =	{Gottlob, Georg},
  title =	{{Artificial Intelligence and Artificial Ignorance}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.3},
  URN =		{urn:nbn:de:0030-drops-196459},
  doi =		{10.4230/LIPIcs.CSL.2024.3},
  annote =	{Keywords: AI applications, symbolic AI, sub-symbolic AI, AI usefulness, achievements of symbolic AI, achievements of machine learning, machine learning errors and mistakes, large language models, LLMs, LLM usefulness, LLM mistakes, inaccuracies}
}
Document
Invited Talk
Approximating Fixpoints of Approximated Functions (Invited Talk)

Authors: Barbara König

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
There is a large body of work on fixpoint theorems, guaranteeing the existence of fixpoints for certain functions and providing methods for computing them. This includes for instance Banachs’s fixpoint theorem, the well-known result by Knaster-Tarski that is frequently employed in computer science and Kleene iteration. It is less clear how to compute fixpoints if the function whose (least) fixpoint we are interested in is not known exactly, but can only be obtained by a sequence of subsequently better approximations. This scenario occurs for instance in the context of reinforcement learning, where the probabilities of a Markov decision process (MDP) - for which one wants to learn a strategy - are unknown and can only be sampled. There are several solutions to this problem where the fixpoint computation (for determining the value vector and the optimal strategy) and the exploration of the model are interleaved. However, these methods work only well for discounted MDPs, that is in the contractive setting, but not for general MDPs, that is for non-expansive functions. After describing and motivating the problem, we will in particular concentrate on the non-expansive case. There are many interesting systems who value vectors can be obtained by determining the fixpoints of non-expansive functions. Other than contractive functions, they do not guarantee uniqueness of the fixpoint, making it more difficult to approximate the least fixpoint by methods other than Kleene iteration. And also Kleene iteration fails if the function under consideration is only approximated. We hence describe a dampened Mann iteration scheme for (higher-dimensional) functions on the reals that converges to the least fixpoint from everywhere. This scheme can also be adapted to functions that are approximated, under certain conditions. We will in particular study the case of MDPs and consider a related problem that arises when performing model-checking for quantitative mu-calculi, which involves the computation of nested fixpoints. This is joint work with Paolo Baldan, Sebastian Gurke, Tommaso Padoan and Florian Wittbold.

Cite as

Barbara König. Approximating Fixpoints of Approximated Functions (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{konig:LIPIcs.CSL.2024.4,
  author =	{K\"{o}nig, Barbara},
  title =	{{Approximating Fixpoints of Approximated Functions}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.4},
  URN =		{urn:nbn:de:0030-drops-196469},
  doi =		{10.4230/LIPIcs.CSL.2024.4},
  annote =	{Keywords: fixpoints, approximation, Markov decision processes}
}
Document
Invited Talk
Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk)

Authors: Marta Kwiatkowska

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
Strategic reasoning is essential to ensure stable multi-agent coordination in complex environments, as it enables synthesis of optimal (or near-optimal) agent strategies and equilibria that guarantee expected outcomes, even in adversarial scenarios. Partially-observable stochastic games (POSGs) are a natural model for real-world settings involving multiple agents, uncertainty and partial information, but lack practical algorithms for computing or approximating optimal values and strategies. Recently, progress has been made for one-sided POSGs, a subclass of two-agent, zero-sum POSGs where only one agent has partial information while the other agent is assumed to have full knowledge of the state, with heuristic search value iteration (HSVI) proposed for computing approximately optimal values and strategies in one-sided POSGs [Horák et al., 2023]. This model is well suited to safety-critical applications, when making worst-case assumptions about one agent; examples include the attacker in a security application, modelled, e.g., as a patrolling or pursuit-evasion game. However, many realistic autonomous coordination scenarios involve agents perceiving continuous environments using data-driven observation functions, typically implemented as neural networks (NNs). Examples include autonomous vehicles using NNs to perform object recognition or to estimate pedestrian intention, or NN-enabled vision in an airborne pursuit-evasion scenario. Such perception mechanisms bring new challenges, notably continuous environments, which are inherently tied to NN-enabled perception because of standard training regimes. This means that naive discretisation is difficult, since decision boundaries obtained for data-driven perception are typically irregular and can be misaligned with gridding schemes for discretisation, affecting the precision of the computed strategies. This invited paper will discuss progress with developing a model class and algorithms for one-sided POSGs with neural perception mechanisms [R. Yan et al., 2022; Yan et al., 2023] that work directly with their continuous state space. Building on continuous-state POMDPs with NN perception mechanisms [Yan et al., 2023], where the key idea is that ReLU neural network classifiers induce a finite decomposition of the continuous environment into polyhedra for each classification label, a piecewise constant representation for the value, reward and perception functions is developed that forms the basis for a variant of HSVI, a point-based solution method that computes a lower and upper bound on the value function from a given belief to compute an (approximately) optimal strategy. We extend these ideas from the single-agent (POMDP) setting [Yan et al., 2023] to zero-sum POSGs. In the game setting, this involves solving a normal form game at each stage and iteration, and goes significantly beyond HSVI for finite POSGs [Horák et al., 2023].

Cite as

Marta Kwiatkowska. Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.CSL.2024.5,
  author =	{Kwiatkowska, Marta},
  title =	{{Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{5:1--5:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.5},
  URN =		{urn:nbn:de:0030-drops-196471},
  doi =		{10.4230/LIPIcs.CSL.2024.5},
  annote =	{Keywords: Stochastic games, neural networks, formal verification, strategy synthesis}
}
Document
Invited Talk
Logical Algorithmics: From Theory to Practice (Invited Talk)

Authors: Moshe Y. Vardi

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
The standard approach to algorithm development is to focus on a specific problem and develop for it a specific algorithm. Codd’s introduction of the relational model in 1970 included two fundamental ideas: (1) Relations provide a universal data representation formalism, and (2) Relational databases can be queried using first-order logic. Realizing these ideas required the development of a meta-algorithm, which takes a declarative query and executes it with respect to a database. In this talk, I will describe this approach, which I call Logical Algorithmics, in detail, and explore its profound ramification.

Cite as

Moshe Y. Vardi. Logical Algorithmics: From Theory to Practice (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.CSL.2024.6,
  author =	{Vardi, Moshe Y.},
  title =	{{Logical Algorithmics: From Theory to Practice}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{6:1--6:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.6},
  URN =		{urn:nbn:de:0030-drops-196494},
  doi =		{10.4230/LIPIcs.CSL.2024.6},
  annote =	{Keywords: Logic, Algorithms}
}
Document
Semantic Bounds and Multi Types, Revisited

Authors: Beniamino Accattoli

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
Intersection types are a standard tool in operational and semantical studies of the λ-calculus. De Carvalho showed how multi types, a quantitative variant of intersection types providing a handy presentation of the relational denotational model, allows one to extract precise bounds on the number of β-steps and the size of normal forms. In the last few years, de Carvalho’s work has been extended and adapted to a number of λ-calculi, evaluation strategies, and abstract machines. These works, however, only adapt the first part of his work, that extracts bounds from multi type derivations, while never consider the second part, which deals with extracting bounds from the multi types themselves. The reason is that this second part is more technical, and requires to reason up to type substitutions. It is however also the most interesting, because it shows that the bounding power is inherent to the relational model (which is induced by the types, without the derivations), independently of its presentation as a type system. Here we dissect and clarify the second part of de Carvalho’s work, establishing a link with principal multi types, and isolating a key property independent of type substitutions.

Cite as

Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.CSL.2024.7,
  author =	{Accattoli, Beniamino},
  title =	{{Semantic Bounds and Multi Types, Revisited}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{7:1--7:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.7},
  URN =		{urn:nbn:de:0030-drops-196504},
  doi =		{10.4230/LIPIcs.CSL.2024.7},
  annote =	{Keywords: Lambda calculus, intersection types, denotational semantics, linear logic}
}
Document
Infinitary Cut-Elimination via Finite Approximations

Authors: Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

Cite as

Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Infinitary Cut-Elimination via Finite Approximations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{acclavio_et_al:LIPIcs.CSL.2024.8,
  author =	{Acclavio, Matteo and Curzi, Gianluca and Guerrieri, Giulio},
  title =	{{Infinitary Cut-Elimination via Finite Approximations}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.8},
  URN =		{urn:nbn:de:0030-drops-196510},
  doi =		{10.4230/LIPIcs.CSL.2024.8},
  annote =	{Keywords: cut-elimination, non-wellfounded proofs, parsimonious logic, linear logic, proof theory, approximation, sequent calculus, non-uniform proofs}
}
Document
Descriptive Complexity for Neural Networks via Boolean Networks

Authors: Veeti Ahvonen, Damian Heiman, and Antti Kuusisto

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
We investigate the descriptive complexity of a class of neural networks with unrestricted topologies and piecewise polynomial activation functions. We consider the general scenario where the running time is unlimited and floating-point numbers are used for simulating reals. We characterize these neural networks with a rule-based logic for Boolean networks. In particular, we show that the sizes of the neural networks and the corresponding Boolean rule formulae are polynomially related. In fact, in the direction from Boolean rules to neural networks, the blow-up is only linear. We also analyze the delays in running times due to the translations. In the translation from neural networks to Boolean rules, the time delay is polylogarithmic in the neural network size and linear in time. In the converse translation, the time delay is linear in both factors. We also obtain translations between the rule-based logic for Boolean networks, the diamond-free fragment of modal substitution calculus and a class of recursive Boolean circuits where the number of input and output gates match.

Cite as

Veeti Ahvonen, Damian Heiman, and Antti Kuusisto. Descriptive Complexity for Neural Networks via Boolean Networks. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{ahvonen_et_al:LIPIcs.CSL.2024.9,
  author =	{Ahvonen, Veeti and Heiman, Damian and Kuusisto, Antti},
  title =	{{Descriptive Complexity for Neural Networks via Boolean Networks}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{9:1--9:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.9},
  URN =		{urn:nbn:de:0030-drops-196528},
  doi =		{10.4230/LIPIcs.CSL.2024.9},
  annote =	{Keywords: Descriptive complexity, neural networks, Boolean networks, floating-point arithmetic, logic}
}
Document
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories

Authors: Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T, where T = IΔ₀+Exp is a well-studied theory based on bounded induction.

Cite as

Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone. Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{antonelli_et_al:LIPIcs.CSL.2024.10,
  author =	{Antonelli, Melissa and Dal Lago, Ugo and Davoli, Davide and Oitavem, Isabel and Pistone, Paolo},
  title =	{{Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.10},
  URN =		{urn:nbn:de:0030-drops-196538},
  doi =		{10.4230/LIPIcs.CSL.2024.10},
  annote =	{Keywords: Bounded Arithmetic, Randomized Computation, Implicit Computational Complexity}
}
  • Refine by Author
  • 29 Silva, Alexandra
  • 6 Kappé, Tobias
  • 5 Bonchi, Filippo
  • 5 Rot, Jurriaan
  • 5 Schmid, Todd
  • Show More...

  • Refine by Classification
  • 20 Theory of computation → Logic and verification
  • 18 Theory of computation → Categorical semantics
  • 14 Theory of computation → Formal languages and automata theory
  • 10 Theory of computation → Finite Model Theory
  • 9 Theory of computation → Design and analysis of algorithms
  • Show More...

  • Refine by Keyword
  • 6 Automata
  • 5 coalgebra
  • 5 completeness
  • 4 Completeness
  • 4 decidability
  • Show More...

  • Refine by Type
  • 186 document
  • 3 volume

  • Refine by Publication Year
  • 87 2022
  • 51 2024
  • 28 2021
  • 6 2023
  • 5 2019
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail