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!

Contact me

• 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.

CV

Download my CV here.

Publications

• “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]

• “Experimenting with superposition in iProver”. In: 26th Automated Reasoning Workshop, London, UK. 2019. [slides]

• “Two Phase Model for Warm Stellar Matter: an Equation of State for Compact Stars”. Master thesis. Universidade de Coimbra, 2017.

See also my dblp and orcid pages.

Other stuff

• TAU-800B Super: An anachronistic computer, in more ways than one.

• quantum-tptp: Automated verification of quantum circuits.

• ocaml-posit: A library for using Type III unums in OCaml. (WIP)

• rprover: An automated theorem prover focusing on extensibility and speed, written in Rust.

• LibriVox: My LibriVox contributions.