18th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA)

is a satellite event of the 8th International Conference on Formal Structures for Computation and Deduction FSCD. The Workshop takes place July 1-2 in Rome, Italy.

Co-organization chairing with Daniele Nantes Sobrinho.

Datasets Generation for Data-Deficient Domains (DG4D^3)

The workshop will take place in Prague, Czechia together with Practical Aspects of Machine Learning in Theorem Proving (PAMLTP) from April 18-20 Webpage. Both events are funded by EUROPROOFNET

Co-chairing with Martin Suda.

36th International Workshop on Unification

The workshop will take place in Haifa, Israel as part of IJCAR 2022 and Federated Logic Conference 2022. More information is availible at https://www.cs.cas.cz/unif-2022/

Co-chairing with Barbara Morawska.

11th International Workshop on Theorem proving components for Educational software

The workshop will take place in Haifa, Israel as part of IJCAR 2022 and Federated Logic Conference 2022. More information is availible at https://www.cs.cas.cz/unif-2022/

Member of the Programming Committee

7th Conference on Artificial Intelligence and Theorem Proving AITP 2022

The workshop will take place in Aussois, France . More information is availible at http://colo12-c703.uibk.ac.at/2022/

Regular participant

15th Conference on Intelligent Computer Mathematics

The workshop will take place in Tbilisi, Georgia. More information is availible at https://cicm-conference.org/2022/cicm.php?event=&menu=general

Member of the Programming Committee

EUROPROOFNET: Short-Term Scientific Mission Grants

Call for short term travel grants every 3 months. More Information can be found here: https://europroofnet.github.io/grants/

Learning to Prove by MATHematical Induction: Invariant Discovery Aided by Modern Machine Learning Technology (MATH LP)

Initially focused on tree grammar based inductive theorem proving, the focus of the project has moved onto Inproving generalization and invariant construction using inductive logic programming method, together with statistical guidance similar to what is currently being used to inprove theorem provers. Project Page

Project Leader, Duration: August 2020 - February 2023

Proof analysis AND Automated deduction FOr REcursive STructures (PANDAFOREST)

The focus of this project is development of a formal framework for the finite representation of Herbrand information extracted from proofs by induction within weak fragments of arithemetics. Project Page

Project Leader, Duration: July 2022 - June 2025