Second Proposal for Reward Bounties
[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:
- Second Proposal for Reward Bounties -
Brown,
2020-10-27, 08:40
![[*]](themes/default/images/complete_thread.png "Open whole thread")
- Second Proposal for Reward Bounties - , 2020-10-27, 12:44
- Second Proposal for Reward Bounties -
,
2020-10-27, 12:53
- Second Proposal for Reward Bounties -
Brown,
2020-10-27, 13:08
- Second Proposal for Reward Bounties - , 2020-10-27, 15:58
- Second Proposal for Reward Bounties -
,
2020-10-27, 16:02
- Second Proposal for Reward Bounties - Brown, 2020-10-28, 15:01
- Second Proposal for Reward Bounties -
Brown,
2020-10-27, 13:08
- Second Proposal for Reward Bounties - Brown, 2020-10-27, 12:58
- Second Proposal for Reward Bounties -
,
2020-10-27, 13:05
- Second Proposal for Reward Bounties - Brown, 2020-10-27, 13:20
- Second Proposal for Reward Bounties - Brown, 2020-12-16, 15:58