Automated deductive reasoning plays an important role in software verification, optimization, and mathematical theorem discovery. This talk explores novel applications and extensions of equality saturation, a technique for efficiently representing and manipulating large sets of equivalent expressions, to enhance automatic deductive reasoning across various domains.
In this talk, we present a collection of three works:
A symbolic theory exploration system, dubbed Thesy, based on equality saturation that efficiently discovers and proves new mathematical lemmas.
By leveraging equality saturation to manipulate symbolic values, TheSy outperforms testing-based approaches in both speed and scope.
The second work is a novel extension to e-graphs, the data structure at the base of the equality saturation technique, enabling efficient conditional reasoning within the equality saturation framework. This memory-efficient approach to representing multiple e-graphs simultaneously opens new avenues for applying equality saturation to complex conditional reasoning problems.
Lastly, we present the Lightweight Equality Saturation (LES) prover. LES utilizes the immense amount of lemmas and definitions available in proof assistant environments, as well as some additional properties resulting from the high-order logic used in these environments to go toe-to-toe with state-of-the-art provers.
These innovations synergize to create a more comprehensive approach to deductive reasoning, from expanding underlying theories to handling conditional logic and enhancing theorem proving capabilities in interactive environments.
