Date: Tuesday, February 20th 2025 – 13h00
Place: A008
Title: The Lisa Proof Assistant & Efficient and Predictable Tools with Orthologic-Based Reasoning
In this talk, I will present my research efforts in improving and developing automated reasoning tools. First, I will present Lisa, a proof assistant based on Set Theory that I am developing. Set Theory has seen little development as foundation of Mathematics in the recent decades, but it offers a greater flexibility than most type-theoretic foundations. Lisa also exploits progress in programming language design to offer more powerful automation capabilities.
Second, I motivate the use of efficient and predictable algorithms as building blocks for automated reasoning tools. Orthologic in particular is a sound approximation to classical logic with polynomial-time validity checking, allowing to solve many propositional transformations. Compared to heuristics, it is guaranteed to be efficient for all tautologies in a well-characterized fragment. Orthologic also admits other interesting properties, such as a normal form, interpolation, and more.
