Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified session_graph_display: restrict sessions to actually required theories;
  3. removed dummy ATP
  4. compile
  5. tuning
  6. invoke remote Vampire with higher-order (THF) syntax
  7. repaired remote_vampire's proof reconstruction
  8. added support for Zipperposition on SystemOnTPTP
  9. folded experimental Ehoh into E now that E 2.3 has been released
  10. removed support for old system E-MaLeS
  11. added support for repote Alt-Ergo
  12. updated nomenclature for TPTP languages to use modern three-symbol abbreviations (e.g. TF1)
  13. removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0
  14. removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
  15. removed support for iProver-Eq
  16. updated iProver setup and tuned other ATP setups
  17. removed experimental encoding for Waldmeister
  18. removed support for remote Satallax because its output does not clearly identify the lemmas used
  19. changed Satallax's setup to invoke E
Changeset 70947:b62bb9a61abc by wenzelm:
merged
Changeset 70946:79d23e6436d0 by wenzelm:
clarified session_graph_display: restrict sessions to actually required theories;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 70945:420f5d1953c7 by blanchet:
removed dummy ATP
The file was removedsrc/HOL/Tools/ATP/scripts/dummy_atp
Changeset 70944:849311b45428 by blanchet:
compile
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Sledgehammer.thy (diff)
Changeset 70943:ccc771091a78 by blanchet:
tuning
The file was modified src/HOL/TPTP/atp_theory_export.ML (diff)
Changeset 70942:718255bde391 by blanchet:
invoke remote Vampire with higher-order (THF) syntax
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70941:d4ef7617e31e by blanchet:
repaired remote_vampire's proof reconstruction
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70940:ce3a05ad07b7 by blanchet:
added support for Zipperposition on SystemOnTPTP
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70939:3218999b3715 by blanchet:
folded experimental Ehoh into E now that E 2.3 has been released
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70938:6d84c3c333d5 by blanchet:
removed support for old system E-MaLeS
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70937:fe114eca312e by blanchet:
added support for repote Alt-Ergo
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70936:646651bcf261 by blanchet:
updated nomenclature for TPTP languages to use modern three-symbol abbreviations (e.g. TF1)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 70935:535ff1eac86c by blanchet:
removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70934:25c1ff13dbdb by blanchet:
removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Sledgehammer.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
Changeset 70933:600da8ccbe5b by blanchet:
removed support for iProver-Eq
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70932:a35618d00d29 by blanchet:
updated iProver setup and tuned other ATP setups
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70931:1d2b2cc792f1 by blanchet:
removed experimental encoding for Waldmeister
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was removedsrc/HOL/Tools/ATP/atp_waldmeister.ML
Changeset 70930:1019b8609552 by blanchet:
removed support for remote Satallax because its output does not clearly identify the lemmas used
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_satallax.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 70929:9b69bb9c1c8d by blanchet:
changed Satallax's setup to invoke E
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)