Hi! My name is André Duarte and I’m currently a PhD researcher on automated theorem proving at the University of Manchester, under the supervision of Prof. Konstantin Korovin. I’m currently focused on efficient ways of dealing with specific hard theories, such as arithmetic or associative-commutative operators, while retaining full completeness and generality for arbitrary problems. My research has applications in domains where these theories are important, such as in formal verification of software, or in theorem proving for mathematics.
Previously I got my BSc and MSc in Physics from the University of Coimbra, with a specialisation in computational physics, having written my thesis on the internal composition of neutron stars.
Feel free to reach out to me with any questions!
- mail [ɑt] andrepd.me (preferred)
- andre.duarte [ɑt] manchester.ac.uk
For encryption, feel free to use this key.
If you’d like to reach me in some other way, please email me and I’ll be glad to exchange some other method of contact.
Download my CV here.
“Ground Joinability and Connectedness in the Superposition Calculus”. In: 11th International Joint Conference on Automated Reasoning, Haifa, Israel. 2022. Best Student Paper award. [slides]
“AC Simplifications and Closure Redundancies in the Superposition Calculus”. In: 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Birmingham, UK. 2021. [slides]
“Implementing Superposition in iProver (System Description)”. In: 10th International Joint Conference on Automated Reasoning, Paris, France. 2020. [slides]
“Two Phase Model for Warm Stellar Matter: an Equation of State for Compact Stars”. Master thesis. Universidade de Coimbra, 2017.
- TAU-800B Super: An anachronistic computer, in more ways than one.