Den Hammer härten: Mehr Integration von automatischen und interaktiven Theorembeweisern

• Antragsteller: Professor Dr. Tobias Nipkow, Ph.D.
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2012 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 226154341

• Erstellungsjahr: 2019

Zusammenfassung der Projektergebnisse

Proof assistants—also called interactive theorem provers—are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, including a verified microkernel, formal theorem proving remains laborious and requires specialized experts. Today it takes novices months or years to become proficient. As one user quipped, “There’s no learning curve—it’s a series of cliffs.” The situation has improved in the past decade with the integration of first-order automatic theorem provers in proof assistant. Sledgehammer is a tool that integrates automatic theorem provers in Isabelle/HOL, a popular proof assistant developed primarily at TU München in the principal investigator’s research group. The primary goal of the Hardening the Hammer project was to increase Sledgehammer’s success rate. During the course of the project, the success rate on a representative set of benchmarks has gone up from 64% to 77%, thanks to various innovations: • the use of machine learning to select potentially relevant lemmas from the available libraries; • the use of lightweight (yet correct) encodings to translate Isabelle’s rich logic to the automatic theorem provers’ less expressive logics; • improvements in the underlying automatic theorem provers, in collaboration with researchers in automated reasoning; • the translation of detailed machine-generated proofs into Isabelle proofs to increase the success rate of proof reconstruction; • the integration of higher-order provers.

Projektbezogene Publikationen (Auswahl)

• Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning 51(1), pp. 109–128, 2013
  Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson
  (Siehe online unter https://doi.org/10.1007/s10817-013-9278-5)
• A learning-based fact selector for Isabelle/HOL. Journal of Automated Reasoning 57(3), pp. 219–244, 2016
  Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban
  (Siehe online unter https://doi.org/10.1007/s10817-016-9362-8)
• Encoding monomorphic and polymorphic types. Logical Methods in Computer Science 12(4:13), 2016, pp. 1–52
  Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone
  (Siehe online unter https://doi.org/10.1007/978-3-642-36742-7_34)
• Hammering towards QED. Journal of Formalized Reasoning 9(1), pp. 101–148, 2016
  Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban
  (Siehe online unter https://doi.org/10.6092/issn.1972-5787/4593)
• Semi-intelligible Isar proofs from machine-generated proofs. Journal of Automated Reasoning 56(2), pp. 155–200, 2016
  Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier
  (Siehe online unter https://doi.org/10.1007/s10817-015-9335-3)
• Superposition: Types and Induction. PhD thesis, Universität des Saarlandes
  Daniel Wand