ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 17:30 - 18:00 at SUN I - SAT Solving and Theorem Proving Chair(s): Armin Biere

Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with a state-of-the-art superposition-based prover, E, and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ-free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone towards full higher-order logic.

Mon 8 Apr
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 18:00: TACAS 2019 - SAT Solving and Theorem Proving at SUN I
Chair(s): Armin BiereJohannes Kepler University Linz
tacas-2019-papers16:30 - 17:00
Pengfei Gao, Hongyi Xie, Jun Zhang, Fu Song, Taolue ChenBirkbeck, University of London
Link to publication
tacas-2019-papers17:00 - 17:30
Wenxi WangThe University of Texas at Austin, Texas, USA, Kaiyuan WangGoogle, Inc., Milos GligoricUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin
Link to publication
tacas-2019-papers17:30 - 18:00
Link to publication