Unification for Subformula Linking under Quantifiers
Subformula linking is a technique that allows one to simplify proof goals by identifying subformulas of hypotheses that share atoms with the goal. It has been used by recent prototypes for gesture-based interactive theorem proving, but also for theorem proving in separation logic.
When linking formulas, we should avoid information loss, i.e., subformula linking should succeed precisely when a provable simplification can be generated. Avoiding information loss is challenging when quantifiers are involved. Existing approaches either generate simplifications that involve equalities, or determine substitutions for variables via unification. The first approach can produce unprovable simplifications, while the second approach can fail to find desired links.
We propose a third approach, called Quantifying on the Uninstantiated (QU), which is also based on unification and lies between the two existing approaches. We show that QU has practical applications for proof automation, by improving tactics for resource framing in the Iris framework for separation logic in Coq.
Tue 16 JanDisplayed time zone: London change
14:00 - 15:30
|Compositional Verification of Concurrent C Programs with Search Structure Templates
Duc-Than Nguyen University of Illinois at Chicago, Lennart Beringer Princeton University, William Mansky University of Illinois Chicago, Shengyi Wang Princeton University, USAPre-print
|Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logicdistinguished paper
Qiyuan Zhao National University of Singapore, George Pîrlea National University of Singapore, Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore, Ilya Sergey National University of SingaporePre-print
|Unification for Subformula Linking under Quantifiers