Second Proposal for Reward Bounties

by , Tuesday, October 27, 2020, 16:02 (404 days ago) @ Brown

[barakeel] The main developer of Coqhammer (Lukasz) told me that it is difficult to get the bushy version (some hacks needed) and the chainy version with premise selection can be produced using https://github.com/lukaszcz/coqhammer/tree/coq8.12/eval/README.md. For Isabelle/HOL, I am not sure I want to get involve into politics. Maybe a better idea would be to take problems from the TPTP library, there should be some Isabelle/HOL problems there too.


Complete thread:

 RSS Feed of thread

powered by my little forum