Local theories and Partial Quantifier Elimination

For my MMath thesis, I mainly worked with first-order theories called, local theories [1], which have interesting proof theoretic and semantic characterizations that lead to polynomial time decidability of the uniform word problem. I identified a subclass of local theories in which we can efficiently do partial quantifier elimination with some completeness guarantees. Using their proof theoretic characterization, I gave a parametrized polynomial time partial quantifier elimination algorithm and showed how it can be applied to arithmetical theories. The paper resulting from this work has been accepted at the Conference on Automated Deduction (CADE).

[1] Harald Ganzinger. 2001. Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01). IEEE Computer Society, USA, 81.

[2] Relatively Complete and Efficient Partial Quantifier Elimination. In Proceedings of the 30th Conference On Automated Deduction (CADE '25')

Logic and Computability Graduate Seminar

My project for the graduate course Logic and Computability was on relative computability, the arithmetical hierarchy, and Post's theorem relating the Turing degrees with the arithmetical hierarchy. The slides from my seminar .

General (Research) Interests

I am generally excited with topics in (mathematical) logic. My fascination with logic started as a philosophical curiosity about the natures of truth and proof. Which (maybe unsurprisingly) led me to appreciate mathematical rigor and problem solving.