This paper introduces slam, an Isabelle/HOL tactic and automated theorem prover based on the λ-superposition calculus. An alternative to Isabelle’s metis tactic, slam targets higher-order logic directly, avoiding the overhead introduced by metis’s translations to first-order logic. Like metis, slam can be used as a Sledgehammer backend to reconstruct proofs produced by external higher-order automated theorem provers such as E, Vampire, and Zipperposition.
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:30 | Proof assistantsCPP at Belvédère Chair(s): Sophie Tourret Inria and Max Planck Institute for Informatics | ||
14:00 22mTalk | A Certifying Proof Assistant for Synthetic Mathematics in Lean CPP Wojciech Nawrocki Carnegie Mellon University, Joseph Hua Carnegie Mellon University, Mario Carneiro Chalmers University of Technology, Yiming Xu LMU Munich, Spencer Woolfson Carnegie Mellon University, Shuge Rong Carnegie Mellon University, Sina Hazratpour Johns Hopkins University, Steve Awodey Carnegie Mellon University | ||
14:22 22mTalk | Adding Sorts to an Isabelle Formalization of Superposition CPP Balazs Toth Ludwig-Maximilians-Universität München, Martin Desharnais Ludwig-Maximilians-Universität München, Jasmin Blanchette Ludwig-Maximilians-Universität München | ||
14:45 22mTalk | A Lambda-Superposition Tactic for Isabelle/HOL CPP Massin Guerdi Ludwig-Maximilians-Universität München | ||
15:07 22mTalk | Certifying the decidability of the word problem in monoids at large CPP Reinis Cirpons St Andrews University, Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA, Assia Mahboubi INRIA, Guillaume Melquiond Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, James Mitchell St Andrews University, Finn Smith St Andrews University | ||