[Master] Decision Procedure for Equivalence Relations
The goal of the proposed research is to design a decision procedure for the Coq/Rocq proof assistant that would extend equality-based reasoning (e.g., congruence-closure) to heterogeneous problems where equalities are expressed using multiple equivalence relations.
Current research has shown that the full quantifier-free problem is undecidable. Therefore it is desirable to understand the limit of the decidability frontier and to identify fragments where the problem remains decidable and heuristics to apply when outside these fragments. Incidently, recent work proves on paper that decidability can indeed be obtained for a fragment where enough base PERs are in fact equivalence relations (i.e. reflexive).
This intern will be tasked with producing:
- a formal definition of the aforementioned decidable fragment
- a formal proof of the decidability result for said fragment.
This Master internship may lead to a PhD proposal.
