Changes

Summary

1. tuned output syntax: Hoare triples are now blocks
2. tuned output syntax: INV and VAR are now blocks
3. more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
4. enable induction in one of Zipperposition's slices
5. made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
6. robustly handle empty proof blocks in Isar proof output
7. propagate right result when enough proofs have been found
8. correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
9. don't lose error messages
10. don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
11. careful with partial applications
12. don't perform preplaying steps if preplaying is disabled
13. adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
14. tuned punctuation
15. handle TPTP '!=' more gracefully in Isar proof reconstruction
16. guard against duplicate lines in Zipperposition proofs
17. tuning
18. tuned NEWS
19. compile HOL-TPTP
20. compile Metis_Examples
21. more NEWS
22. compile mirabelle
23. tweaked Auto Sledgehammer's behavior and output
24. updated NEWS
25. removed experimental prover z3_tptp
26. print more verbose information
27. run all installed provers by default
28. update slice options centrally
29. further work on new Sledgehammer slicing
30. tweaked verbose output
31. tweak padding of prover slice schedule to include all provers
32. implemented 'max_proofs' mechanism
33. document new option 'max_proofs'
34. crude implementation of centralized slicing
35. removed obscure E option
36. take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
37. rationalize slicing format
38. thread slices through
39. simplified 'best_slice' data structure and made minor changes to slices
40. changed logic of 'slice' option to 'slices'
41. updated documentation of 'slice' (now 'slices') option
42. revised Sledgehammer documentation
43. rationalized output for forthcoming slicing model
44. use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
45. disable slicing within ATP module (in preparation for refactoring)
46. disable slicing within SMT (in preparation for factoring it out)
47. generalized the 'slice' option towards more flexible slicing
48. tuned -- fewer warnings;

Summary

1. Strong soundness.
2. Strong soundness.
3. Fix LaTeX issue.
4. Qualification required(?)
5. merged
6. more variants of the algorithm
7. Added funding acknowledgments. Fixed broken BibTeX citation.
8. Strong completeness for PAL systems.