Foundations for Natural Proofs and Quantifier Instantiation

Watch a 25-minute conference presentation from POPL 2018 exploring foundational results in first-order logic (FOL) and verification. Discover how systematic term instantiation achieves completeness for a "safe" fragment of FOL, providing theoretical backing for heuristic approaches used in heap verification engines. Learn about the relationship between unfolding recursive definitions and term instantiation, and examine how introducing induction principles can help bridge FOL with recursive definitions. The presentation, delivered by researchers from RWTH Aachen University and the University of Illinois at Urbana-Champaign, offers valuable insights for those interested in program analysis, verification, and program logics.