3 Search Results for "Negri, Sara"


Document
Constructive Cut Elimination in Geometric Logic

Authors: Giulio Fellin, Sara Negri, and Eugenio Orlandelli

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)


Abstract
A constructivisation of the cut-elimination proof for sequent calculi for classical and intuitionistic infinitary logic with geometric rules - given in earlier work by the second author - is presented. This is achieved through a procedure in which the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. Additionally, a proof of Barr’s Theorem for geometric theories that uses only constructively acceptable proof-theoretical tools is obtained.

Cite as

Giulio Fellin, Sara Negri, and Eugenio Orlandelli. Constructive Cut Elimination in Geometric Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{fellin_et_al:LIPIcs.TYPES.2021.7,
  author =	{Fellin, Giulio and Negri, Sara and Orlandelli, Eugenio},
  title =	{{Constructive Cut Elimination in Geometric Logic}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.7},
  URN =		{urn:nbn:de:0030-drops-167763},
  doi =		{10.4230/LIPIcs.TYPES.2021.7},
  annote =	{Keywords: Geometric theories, sequent calculi, axioms-as-rules, infinitary logic, constructive cut elimination}
}
Document
Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)

Authors: Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster

Published in: Dagstuhl Reports, Volume 11, Issue 10 (2022)


Abstract
At least from a practical and contemporary angle, the time-honoured question about the extent of intuitionistic mathematics rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. All this is ideally done by manipulating proofs mechanically or by adequate metatheorems, which includes proof translations, automated theorem proving, program extraction from proofs, proof analysis and proof mining. The question should thus be put as: What is the computational content of proofs? Guided by this central question, the present Dagstuhl seminar puts a special focus on coherent and geometric theories and their generalisations. These are not only widespread in mathematics and non-classical logics such as temporal and modal logics, but also a priori amenable for constructivisation, e.g., by Barr’s Theorem, and last but not least particularly suited as a basis for automated theorem proving. Specific topics include categorical semantics for geometric theories, complexity issues of and algorithms for geometrisation of theories including speed-up questions, the use of geometric theories in constructive mathematics including finding algorithms, proof-theoretic presentation of sheaf models and higher toposes, and coherent logic for automatically readable proofs.

Cite as

Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster. Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). In Dagstuhl Reports, Volume 11, Issue 10, pp. 151-172, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{coquand_et_al:DagRep.11.10.151,
  author =	{Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
  title =	{{Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)}},
  pages =	{151--172},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{10},
  editor =	{Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.11.10.151},
  URN =		{urn:nbn:de:0030-drops-159321},
  doi =		{10.4230/DagRep.11.10.151},
  annote =	{Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory}
}
Document
What Makes Spatial Data Big? A Discussion on How to Partition Spatial Data

Authors: Alberto Belussi, Damiano Carra, Sara Migliorini, Mauro Negri, and Giuseppe Pelagatti

Published in: LIPIcs, Volume 114, 10th International Conference on Geographic Information Science (GIScience 2018)


Abstract
The amount of available spatial data has significantly increased in the last years so that traditional analysis tools have become inappropriate to effectively manage them. Therefore, many attempts have been made in order to define extensions of existing MapReduce tools, such as Hadoop or Spark, with spatial capabilities in terms of data types and algorithms. Such extensions are mainly based on the partitioning techniques implemented for textual data where the dimension is given in terms of the number of occupied bytes. However, spatial data are characterized by other features which describe their dimension, such as the number of vertices or the MBR size of geometries, which greatly affect the performance of operations, like the spatial join, during data analysis. The result is that the use of traditional partitioning techniques prevents to completely exploit the benefit of the parallel execution provided by a MapReduce environment. This paper extensively analyses the problem considering the spatial join operation as use case, performing both a theoretical and an experimental analysis for it. Moreover, it provides a solution based on a different partitioning technique, which splits complex or extensive geometries. Finally, we validate the proposed solution by means of some experiments on synthetic and real datasets.

Cite as

Alberto Belussi, Damiano Carra, Sara Migliorini, Mauro Negri, and Giuseppe Pelagatti. What Makes Spatial Data Big? A Discussion on How to Partition Spatial Data. In 10th International Conference on Geographic Information Science (GIScience 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 114, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{belussi_et_al:LIPIcs.GISCIENCE.2018.2,
  author =	{Belussi, Alberto and Carra, Damiano and Migliorini, Sara and Negri, Mauro and Pelagatti, Giuseppe},
  title =	{{What Makes Spatial Data Big? A Discussion on How to Partition Spatial Data}},
  booktitle =	{10th International Conference on Geographic Information Science (GIScience 2018)},
  pages =	{2:1--2:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-083-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{114},
  editor =	{Winter, Stephan and Griffin, Amy and Sester, Monika},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GISCIENCE.2018.2},
  URN =		{urn:nbn:de:0030-drops-93306},
  doi =		{10.4230/LIPIcs.GISCIENCE.2018.2},
  annote =	{Keywords: Spatial join, SpatialHadoop, MapReduce, partitioning, big data}
}
  • Refine by Author
  • 2 Negri, Sara
  • 1 Belussi, Alberto
  • 1 Carra, Damiano
  • 1 Coquand, Thierry
  • 1 Fellin, Giulio
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Proof theory
  • 1 Information systems → Geographic information systems
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Constructive mathematics

  • Refine by Keyword
  • 1 Geometric theories
  • 1 MapReduce
  • 1 Spatial join
  • 1 SpatialHadoop
  • 1 automated theorem proving
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2022
  • 1 2018

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