Literature study: Hammering towards QED

Gives an overview of the history, development, architecture and performance of Hammers (Sledgehammer, HOLyHammer, MizAR) throughout early developments up until 2016.

Architecture: lemma selection, problem translation, proof reconstruction
Talks about the techniques and issues with each, mostly focusing on higher-order logic based ITPs; does not go into detail about type-theory based provers (Agda, Coq, **Lean**).


id: 25bc7cb6c397459888ffc9eb35f5ec22
parent_id: ea739ea32b9a4a8ebf7c2355b78c9cf4
created_time: 2023-03-31T14:43:53.803Z
updated_time: 2023-04-07T20:12:58.946Z
is_conflict: 0
latitude: 52.01157690
longitude: 4.35706770
altitude: 0.0000
author: 
source_url: 
is_todo: 0
todo_due: 0
todo_completed: 0
source: joplin-desktop
source_application: net.cozic.joplin-desktop
application_data: 
order: 0
user_created_time: 2023-03-31T14:43:53.803Z
user_updated_time: 2023-04-07T20:12:58.946Z
encryption_cipher_text: 
encryption_applied: 0
markup_language: 1
is_shared: 0
share_id: 
conflict_original_id: 
master_key_id: 
type_: 1