europroofnet / europroofnet.github.io Goto Github PK

In the working groups page the link for WG4 points to the description of WG6.

• 22-23 April 2024: Workshop on Theory and Applications of Craig Interpolation and Beth Definability (CIBD 2024), Amsterdam, Netherlands

Could you please introduce the two following publications?

• @inproceedings{DBLP:conf/isaim/AransayLMR22,
  author = {Jesús Aransay and Laureano Lambán and Julius Michaelis and Julio Rubio},
  title = {Formalizing Alexander duality through BDDs},
  booktitle = {Proceedings of the International Symposium on Artificial Intelligence
  and Mathematics 2022 {(ISAIM} 2022), Fort Lauderdale, Florida, USA,
  January 3-5, 2022},
  year = {2022},
  url = {https://isaim2022.cs.ou.edu/papers/ISAIM2022\_Formalization\_Aransay\_et\_al.pdf},
  timestamp = {Fri, 25 Feb 2022 12:04:56 +0100},
  biburl = {https://dblp.org/rec/conf/isaim/AransayLMR22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
  }

• @inproceedings{DBLP:conf/mkm/AransayLR23,
  author = {Jesús Aransay and Laureano Lambán and Julio Rubio},
  editor = {Catherine Dubois and Manfred Kerber},
  title = {Evasiveness Through Binary Decision Diagrams},
  booktitle = {Intelligent Computer Mathematics - 16th International Conference,
  {CICM} 2023, Cambridge, UK, September 5-8, 2023, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {14101},
  pages = {37--52},
  publisher = {Springer},
  year = {2023},
  url = {https://doi.org/10.1007/978-3-031-42753-4\_3},
  doi = {10.1007/978-3-031-42753-4_3},
  timestamp = {Tue, 05 Sep 2023 20:33:24 +0200},
  biburl = {https://dblp.org/rec/conf/mkm/AransayLR23.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
  }

Thank you in advance!!

Jesús

A problems database for Geometry

TGTP, Thousand of Geometric problems for geometric Theorem Provers

http://hilbert.mat.uc.pt/TGTP/index.php

Pedro Quaresma, University of Coimbra

Please feel free to add the following paper to EuroProofNet publication list:

@Article{maggesi2023mechanising,
title={Mechanising {G}{"o}del--{L}{"o}b {P}rovability {L}ogic in {HOL} {L}ight},
author={Maggesi, Marco and Perini Brogi, Cosimo},
journal={Journal of Automated Reasoning},
volume={67},
number={3},
pages={29},
year={2023},
publisher={Springer}
}

Please feel free to add the following publication:

@inproceedings{DBLP:conf/frocos/TorstenssonW23,
author = {Olle Torstensson and
Tjark Weber},
editor = {Uli Sattler and
Martin Suda},
title = {Hammering Floating-Point Arithmetic},
booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS
2023, Prague, Czech Republic, September 20-22, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14279},
pages = {217--235},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43369-6\_12},
doi = {10.1007/978-3-031-43369-6_12},
timestamp = {Sun, 24 Sep 2023 15:46:26 +0200},
biburl = {https://dblp.org/rec/conf/frocos/TorstenssonW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

Title

We have a research group that can be called

Type theory group at University of Warsaw

Currently we do not have a web page.

Here are some papers published in 2022-2023 that I co-authored and they are related to the action:

@Article{DBLP:journals/jlap/ChenLR23,
author = {Xiaohong Chen and
Dorel Lucanu and
Grigore Rosu},
title = {Capturing constrained constructor patterns in matching logic},
journal = {J. Log. Algebraic Methods Program.},
volume = {130},
pages = {100810},
year = {2023},
url = {https://doi.org/10.1016/j.jlamp.2022.100810},
doi = {10.1016/j.jlamp.2022.100810},
timestamp = {Mon, 28 Aug 2023 21:32:06 +0200},
biburl = {https://dblp.org/rec/journals/jlap/ChenLR23.bib},
bib source = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/corr/abs-2309-13798,
author = {Dorel Lucanu},
title = {Matching-Logic-Based Understanding of Polynomial Functors and their
Initial/Final Models},
journal = {CoRR},
volume = {abs/2309.13798},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2309.13798},
doi = {10.48550/arXiv.2309.13798},
eprinttype = {arXiv},
eprint = {2309.13798},
timestamp = {Wed, 27 Sep 2023 16:51:35 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2309-13798.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ictac/Alexandru-IoanL22,
author = {Lungu Alexandru{-}Ioan and
Dorel Lucanu},
editor = {Helmut Seidl and
Zhiming Liu and
Corina S. Pasareanu},
title = {A Matching Logic Foundation for Alk},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2022 - 19th International
Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13572},
pages = {290--304},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-17715-6\_19},
doi = {10.1007/978-3-031-17715-6_19},
timestamp = {Fri, 07 Oct 2022 16:33:00 +0200},
biburl = {https://dblp.org/rec/conf/ictac/Alexandru-IoanL22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{CIOBACA2023100894,
title = {Operationally-based program equivalence proofs using LCTRSs},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {135},
pages = {100894},
year = {2023},
issn = {2352-2208},
doi = {https://doi.org/10.1016/j.jlamp.2023.100894},
url = {https://www.sciencedirect.com/science/article/pii/S2352220823000482},
author = {Ştefan Ciobâcă and Dorel Lucanu and Andrei Sebastian Buruiană}
}

@Inproceedings{EPTCS389.4,
author = {Lucanu, Dorel},
year = {2023},
title = {Matching-Logic-Based Understanding of Polynomial Functors and their Initial/Final Models},
editor = {Cheval, Hora\c{t}iu and Leu\c{s}tean, Lauren\c{t}iu and Sipo\c{s}, Andrei},
booktitle = {{\rm Proceedings 7th Symposium on}
Working Formal Methods,
{\rm Bucharest, Romania, 21-22 September 2023}},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {389},
publisher = {Open Publishing Association},
pages = {41-55},
doi = {10.4204/EPTCS.389.4},
}

@inproceedings{DBLP:journals/corr/abs-2110-11700,
author = {Andrei Arusoaie and
Dorel Lucanu},
editor = {Vlad Rusu},
title = {Proof-Carrying Parameters in Certified Symbolic Execution: The Case
Study of Antiunification},
booktitle = {Proceedings of the Sixth Working Formal Methods Symposium, {FROM}
2022, "Al. I. Cuza University", Iasi, Romania, 19-20 September, 2022},
series = {{EPTCS}},
volume = {369},
pages = {1--16},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.369.1},
doi = {10.4204/EPTCS.369.1},
timestamp = {Mon, 28 Aug 2023 21:26:21 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2110-11700.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

A paper in the ThEdu'21/EPTCS 354 - Automated Deduction in Secondary Schools

Quaresma, Pedro and Santos, Vanda Four Geometry Problems to Introduce Automated Deduction in Secondary Schools, Proceedings 10th International Workshop on Theorem Proving Components for Educational Software, EPTCS 354, pp. 27--42 2022. DOI: 10.4204/EPTCS.354.3

Pedro Quaresma, University of Coimbra

We have a conference paper and a journal paper to include in the scientific report. The references are these ones:

Montserrat Hermo, Paqui Lucio, César Sánchez: Tableaux for Realizability of Safety Specifications. Formal Methods 2023, pp: 495-513.

Alex Abuin, Alexander Bolotov, Montserrat Hermo, Paqui Lucio: Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models. J. Log. Algebraic Methods Program. 130: 100828 (2023).

Montserrat Hermo

A chapter of a (Springer) book reviewing the area of automated deduction and dynamic construction in geometry.

Quaresma, Pedro, Evolution of Automated Deduction and Dynamic Constructions in Geometry, in Mathematics education in the age of Artificial intelligence, chp. 1, pp. 3--22, Mathematics Education in the Digital Era, Springer, 2022. DOI: 10.1007/978-3-030-86909-0

Pedro Quaresma, University of Coimbra