8 Search Results for "Rodríguez, Leonardo"

Document
DOI: 10.4230/LIPIcs.ESA.2025.97
A Fast and Simple Algorithm for the Resource Constrained Shortest Path Problem

Authors: Saman Ahmadi, Andrea Raith, and Mahdi Jalili

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
Constrained pathfinding is a classic yet challenging network optimization problem with broad applicability across many real-world domains. The Resource-Constrained Shortest Path (RCSP) problem focuses on finding cost-optimal paths that satisfy multiple resource constraints. In this paper, we propose a novel heuristic-guided search framework that accelerates constrained search in large-scale networks, including those with negative costs and resources, by leveraging efficient queuing and pruning strategies. Experimental results on real-world benchmark maps show that our framework achieves up to two orders of magnitude speedup over state-of-the-art methods, demonstrating its effectiveness in solving challenging RCSP instances within limited time.
Cite as

Saman Ahmadi, Andrea Raith, and Mahdi Jalili. A Fast and Simple Algorithm for the Resource Constrained Shortest Path Problem. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 97:1-97:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ahmadi_et_al:LIPIcs.ESA.2025.97,
  author =	{Ahmadi, Saman and Raith, Andrea and Jalili, Mahdi},
  title =	{{A Fast and Simple Algorithm for the Resource Constrained Shortest Path Problem}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{97:1--97:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.97},
  URN =		{urn:nbn:de:0030-drops-245668},
  doi =		{10.4230/LIPIcs.ESA.2025.97},
  annote =	{Keywords: constrained pathfinding, shortest path problem, heuristic search}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.37
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)

Authors: Eric Vin, Kyle A. Miller, and Daniel J. Fremont

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean’s existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications.
Cite as

Eric Vin, Kyle A. Miller, and Daniel J. Fremont. LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 37:1-37:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vin_et_al:LIPIcs.ITP.2025.37,
  author =	{Vin, Eric and Miller, Kyle A. and Fremont, Daniel J.},
  title =	{{LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{37:1--37:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.37},
  URN =		{urn:nbn:de:0030-drops-246356},
  doi =		{10.4230/LIPIcs.ITP.2025.37},
  annote =	{Keywords: Linear Temporal Logic, Interactive Theorem Proving, Lean 4}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.18
Advancing Intelligent Personal Assistants for Human Spaceflight

Authors: Leonie Bensch, Oliver Bensch, and Tommy Nilsson

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
The Artemis program and upcoming missions to Mars mark a new era of human space exploration that will require new tools to support astronaut autonomy in the absence of real-time communication with Earth. This paper investigates the role of voice-based intelligent personal assistants (IPAs) in future crewed space missions. Through semi-structured interviews with astronauts (n=3) and spaceflight experts (n=12), we identify key user-centered design requirements for IPAs in this uniquely constrained and safety-critical environment. Our thematic analysis reveals core requirements for flexibility, reliability, offline capability, and multimodal interaction. Drawing on these findings, we outline design guidelines for next-generation IPAs and discuss how technologies such as retrieval-augmented generation (RAG), knowledge graphs, and augmented reality should be combined to support flexible, reliable, and multimodal IPAs for future human spaceflight missions.
Cite as

Leonie Bensch, Oliver Bensch, and Tommy Nilsson. Advancing Intelligent Personal Assistants for Human Spaceflight. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bensch_et_al:OASIcs.SpaceCHI.2025.18,
  author =	{Bensch, Leonie and Bensch, Oliver and Nilsson, Tommy},
  title =	{{Advancing Intelligent Personal Assistants for Human Spaceflight}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{18:1--18:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.18},
  URN =		{urn:nbn:de:0030-drops-240082},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.18},
  annote =	{Keywords: Conversational Assistant, Intelligent Personal Assistant, Artificial Intelligence, Astronaut, Human Spaceflight, Generative Pre-Trained Transformer (GPT), Retrieval Augmented Generation (RAG), Knowledge Graphs, Augmented Reality, Voice Assistant, Long Duration Spaceflight}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.33
Constraint-Based In-Station Train Dispatching

Authors: Andreas Schutt, Matteo Cardellini, Jip J. Dekker, Daniel Harabor, Marco Maratea, and Mauro Vallati

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
In-station dispatching is the problem of planning the movements of scheduled trains inside a railway station. Effective solutions for in-station dispatching are important for maximising the utilisation of railway infrastructure and for mitigating the impact of incidents and delays in the broader network. In this paper, we explore a constraint-based approach to perform in-station train dispatching. Our extensive empirical analysis of multiple modelling, search strategy, and solver choices, performed over synthetically generated, yet realistic, data, shows that our method outperforms the existing planning-based state-of-the-art approach. In addition, we present different optimisation criteria, which can be effortless defined thanks to the constraint-based approach.
Cite as

Andreas Schutt, Matteo Cardellini, Jip J. Dekker, Daniel Harabor, Marco Maratea, and Mauro Vallati. Constraint-Based In-Station Train Dispatching. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schutt_et_al:LIPIcs.CP.2025.33,
  author =	{Schutt, Andreas and Cardellini, Matteo and Dekker, Jip J. and Harabor, Daniel and Maratea, Marco and Vallati, Mauro},
  title =	{{Constraint-Based In-Station Train Dispatching}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{33:1--33:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.33},
  URN =		{urn:nbn:de:0030-drops-238941},
  doi =		{10.4230/LIPIcs.CP.2025.33},
  annote =	{Keywords: in-station train dispatching, train scheduling, railway scheduling, constraint programming, mixed-integer programming}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.4
Conflict Analysis Based on Cutting-Planes for Constraint Programming

Authors: Robbin Baauw, Maarten Flippo, and Emir Demirović

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
This paper introduces a novel constraint learning mechanism for Constraint Programming (CP) solvers that integrates cutting planes reasoning into the conflict analysis procedure. Drawing inspiration from Lazy Clause Generation (LCG), our approach, named Lazy Linear Generation (LLG), can generate linear integer inequalities to prune the search space, rather than propositional clauses as in LCG. This combines the strengths of constraint programming (strong propagation through global constraints) with cutting-planes reasoning. We present linear constraint explanations for various arithmetic constraints and the element constraint. An experimental evaluation shows that the improved generality of linear constraints has a practical impact on a CP solver by reducing the number of encountered conflicts in 45% of our benchmark instances. Our analysis and prototype implementation show promising results and are an important step towards a new paradigm to make constraint programming solvers more effective.
Cite as

Robbin Baauw, Maarten Flippo, and Emir Demirović. Conflict Analysis Based on Cutting-Planes for Constraint Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baauw_et_al:LIPIcs.CP.2025.4,
  author =	{Baauw, Robbin and Flippo, Maarten and Demirovi\'{c}, Emir},
  title =	{{Conflict Analysis Based on Cutting-Planes for Constraint Programming}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.4},
  URN =		{urn:nbn:de:0030-drops-238655},
  doi =		{10.4230/LIPIcs.CP.2025.4},
  annote =	{Keywords: constraint programming, learning, conflict analysis}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.23
Symbolic Conflict Analysis in Pseudo-Boolean Optimization

Authors: Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
In the the last two decades, a lot of effort has been devoted to the development of satisfiability-checking tools for a variety of SAT-related problems. However, most of these tools lack optimization capabilities. That is, instead of finding any solution, one is sometimes interested in a solution that is best according to some criterion. Pseudo-Boolean solvers can be used to deal with optimization by successively solving a series of problems that contain an additional pseudo-Boolean constraint expressing that a better solution is required. A key point for the success of this simple approach is that lemmas that are learned for one problem can be reused for subsequent ones. In this paper we go one step further and show how, by using a simple symbolic conflict analysis procedure, not only can lemmas be reused between problems but also strengthened, thus further pruning the search space traversal. In addition, we show how this technique automatically allows one to infer upper bounds in maximization problems, thus giving an estimation of how far the solver is from finding an optimal solution. Experimental results with our PB solver reveal that (i) this technique is indeed effective in practice, providing important speedups in problems where several solutions are found and (ii) on problems with very few solutions, where the impact of our technique is limited, its overhead is negligible.
Cite as

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Symbolic Conflict Analysis in Pseudo-Boolean Optimization. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2025.23,
  author =	{Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui},
  title =	{{Symbolic Conflict Analysis in Pseudo-Boolean Optimization}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.23},
  URN =		{urn:nbn:de:0030-drops-237579},
  doi =		{10.4230/LIPIcs.SAT.2025.23},
  annote =	{Keywords: SAT, Pseudo-Boolean Optimization, Conflict Analysis}
}
Document
Position
DOI: 10.4230/TGDK.1.1.2
Large Language Models and Knowledge Graphs: Opportunities and Challenges

Authors: Jeff Z. Pan, Simon Razniewski, Jan-Christoph Kalo, Sneha Singhania, Jiaoyan Chen, Stefan Dietze, Hajira Jabeen, Janna Omeliyanenko, Wen Zhang, Matteo Lissandrini, Russa Biswas, Gerard de Melo, Angela Bonifati, Edlira Vakaj, Mauro Dragoni, and Damien Graux

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Large Language Models (LLMs) have taken Knowledge Representation - and the world - by storm. This inflection point marks a shift from explicit knowledge representation to a renewed focus on the hybrid representation of both explicit knowledge and parametric knowledge. In this position paper, we will discuss some of the common debate points within the community on LLMs (parametric knowledge) and Knowledge Graphs (explicit knowledge) and speculate on opportunities and visions that the renewed focus brings, as well as related research topics and challenges.
Cite as

Jeff Z. Pan, Simon Razniewski, Jan-Christoph Kalo, Sneha Singhania, Jiaoyan Chen, Stefan Dietze, Hajira Jabeen, Janna Omeliyanenko, Wen Zhang, Matteo Lissandrini, Russa Biswas, Gerard de Melo, Angela Bonifati, Edlira Vakaj, Mauro Dragoni, and Damien Graux. Large Language Models and Knowledge Graphs: Opportunities and Challenges. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 2:1-2:38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{pan_et_al:TGDK.1.1.2,
  author =	{Pan, Jeff Z. and Razniewski, Simon and Kalo, Jan-Christoph and Singhania, Sneha and Chen, Jiaoyan and Dietze, Stefan and Jabeen, Hajira and Omeliyanenko, Janna and Zhang, Wen and Lissandrini, Matteo and Biswas, Russa and de Melo, Gerard and Bonifati, Angela and Vakaj, Edlira and Dragoni, Mauro and Graux, Damien},
  title =	{{Large Language Models and Knowledge Graphs: Opportunities and Challenges}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{2:1--2:38},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.2},
  URN =		{urn:nbn:de:0030-drops-194766},
  doi =		{10.4230/TGDK.1.1.2},
  annote =	{Keywords: Large Language Models, Pre-trained Language Models, Knowledge Graphs, Ontology, Retrieval Augmented Language Models}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.230
A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language

Authors: Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
In this paper we present a compiler that translates programs from an imperative higher-order language into a sequence of instructions for an abstract machine. We consider an extension of the Krivine machine for the call-by-name lambda calculus, which includes strict operators and imperative features. We show that the compiler is correct with respect to the big-step semantics of our language, both for convergent and divergent programs.
Cite as

Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano. A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 230-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{rodriguez_et_al:LIPIcs.TYPES.2013.230,
  author =	{Rodr{\'\i}guez, Leonardo and Fridlender, Daniel and Pagano, Miguel},
  title =	{{A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{230--250},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.230},
  URN =		{urn:nbn:de:0030-drops-46343},
  doi =		{10.4230/LIPIcs.TYPES.2013.230},
  annote =	{Keywords: Abstract Machines, Compiler Correctness, Big-step semantics}
}
  • Refine by Type
  • 8 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 6 2025
  • 1 2023
  • 1 2014

  • Refine by Author
  • 1 Ahmadi, Saman
  • 1 Baauw, Robbin
  • 1 Bensch, Leonie
  • 1 Bensch, Oliver
  • 1 Biswas, Russa
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 1 OASIcs
  • 1 TGDK

  • Refine by Classification
  • 1 Applied computing → Operations research
  • 1 Computing methodologies → Intelligent agents
  • 1 Computing methodologies → Knowledge representation and reasoning
  • 1 Computing methodologies → Natural language processing
  • 1 Computing methodologies → Planning and scheduling
  • Show More...

  • Refine by Keyword
  • 2 Knowledge Graphs
  • 2 constraint programming
  • 1 Abstract Machines
  • 1 Artificial Intelligence
  • 1 Astronaut
  • 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