Disequalities in E-Graphs: An Experiment

Explore the integration of disequalities into e-graphs for enhancing automated theorem provers in this 25-minute video presentation from the EGRAPHS 2024 workshop. Delve into two existing approaches implemented in the egg e-graph library, examining preliminary results on their effectiveness. Learn about the feasibility of integrating disequalities into e-graphs using egg, with promising findings suggesting improved efficiency in proof search algorithms. Discover the researchers' plans to refine this approach, integrate it into the Propel automated theorem prover, and make their extensions to egg available to the research community. Gain insights from George Zakhour, Pascal Weisenburger, and Guido Salvaneschi from the University of St. Gallen as they present their experiment on disequalities in e-graphs.