3 Search Results for "Parent, Alex"

Document
DOI: 10.4230/LIPIcs.CSL.2026.18
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.
Cite as

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
  author =	{Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{18:1--18:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.18},
  URN =		{urn:nbn:de:0030-drops-254427},
  doi =		{10.4230/LIPIcs.CSL.2026.18},
  annote =	{Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}
Document
DOI: 10.4230/LIPIcs.GIScience.2025.2
CityJSON Management Using Multi-Model Graph Database to Support 3D Urban Data Management

Authors: Muhammad Syafiq, Suhaibah Azri, and Uznir Ujang

Published in: LIPIcs, Volume 346, 13th International Conference on Geographic Information Science (GIScience 2025)

Abstract
The prevalence of 3D city models in urban applications is increasing due to their lightweight and flexibility, making them adaptable to various applications. However, effective data interoperability remains an issue. Managing 3D city models within a database can improve urban data management applications such as data enrichment and efficient querying. Motivated by the need for better interoperability of 3D city models, this paper proposes a novel method for storing CityJSON using the concept of a multi-model graph database as a foundation for enriching its semantics. The proposed approach involves decomposing CityJSON objects into smaller JSON components, which are then abstracted into graph elements. Parent-child and other relationship attributes are modelled to capture the hierarchical and associative structures of the CityJSON data. A specific programme is employed to preprocess CityJSON data based on several conditions before being loaded into the graph database. Our multi-model approach allows three types of queries: document, graph, and hybrid. The latter combines both document and graph query. Comparative evaluation against relational databases demonstrates that the proposed method outperforms in terms of query performance. The improved query performance is attributed to the advantage of graph database that reduces the need for joins and the ability to efficiently index and navigate JSON data. The findings of this study establish a foundation for semantic enrichment of 3D city models to improve interoperability and support advanced urban data management.
Cite as

Muhammad Syafiq, Suhaibah Azri, and Uznir Ujang. CityJSON Management Using Multi-Model Graph Database to Support 3D Urban Data Management. In 13th International Conference on Geographic Information Science (GIScience 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 346, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{syafiq_et_al:LIPIcs.GIScience.2025.2,
  author =	{Syafiq, Muhammad and Azri, Suhaibah and Ujang, Uznir},
  title =	{{CityJSON Management Using Multi-Model Graph Database to Support 3D Urban Data Management}},
  booktitle =	{13th International Conference on Geographic Information Science (GIScience 2025)},
  pages =	{2:1--2:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-378-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{346},
  editor =	{Sila-Nowicka, Katarzyna and Moore, Antoni and O'Sullivan, David and Adams, Benjamin and Gahegan, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2025.2},
  URN =		{urn:nbn:de:0030-drops-238310},
  doi =		{10.4230/LIPIcs.GIScience.2025.2},
  annote =	{Keywords: CityJSON, Graph Database, 3D City Model, 3D GIS, Interoperability}
}
Document
DOI: 10.4230/LIPIcs.TQC.2017.7
Improved reversible and quantum circuits for Karatsuba-based integer multiplication

Authors: Alex Parent, Martin Roetteler, and Michele Mosca

Published in: LIPIcs, Volume 73, 12th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2017)

Abstract
Integer arithmetic is the underpinning of many quantum algorithms, with applications ranging from Shor's algorithm over HHL for matrix inversion to Hamiltonian simulation algorithms. A basic objective is to keep the required resources to implement arithmetic as low as possible. This applies in particular to the number of qubits required in the implementation as for the foreseeable future this number is expected to be small. We present a reversible circuit for integer multiplication that is inspired by Karatsuba's recursive method. The main improvement over circuits that have been previously reported in the literature is an asymptotic reduction of the amount of space required from O(n^1.585) to O(n^1.427). This improvement is obtained in exchange for a small constant increase in the number of operations by a factor less than 2 and a small asymptotic increase in depth for the parallel version. The asymptotic improvement are obtained from analyzing pebble games on complete ternary trees.
Cite as

Alex Parent, Martin Roetteler, and Michele Mosca. Improved reversible and quantum circuits for Karatsuba-based integer multiplication. In 12th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 73, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parent_et_al:LIPIcs.TQC.2017.7,
  author =	{Parent, Alex and Roetteler, Martin and Mosca, Michele},
  title =	{{Improved reversible and quantum circuits for Karatsuba-based integer multiplication}},
  booktitle =	{12th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2017)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-034-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{73},
  editor =	{Wilde, Mark M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2017.7},
  URN =		{urn:nbn:de:0030-drops-85841},
  doi =		{10.4230/LIPIcs.TQC.2017.7},
  annote =	{Keywords: Quantum algorithms, reversible circuits, quantum circuits, integer multiplication, pebble games, Karatsuba's method}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2018

  • Refine by Author
  • 1 Azri, Suhaibah
  • 1 Bilotta, Antonella
  • 1 Maggesi, Marco
  • 1 Mosca, Michele
  • 1 Parent, Alex
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 1 Information systems → Database design and models
  • 1 Information systems → Geographic information systems
  • 1 Information systems → Graph-based database models
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Higher order logic
  • Show More...

  • Refine by Keyword
  • 1 3D City Model
  • 1 3D GIS
  • 1 Automated proof-search
  • 1 CityJSON
  • 1 Graph Database
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact