FOL/SMT classical tools support?

[brando90]

I know Lean is a higher order logic...but it would be nice to have a benchmark where classical SMT methods can be benchmarked too. What is the possibility/effort/path to translate miniF2F to a format compatible with classical SMT/ATP solvers?

[DyeKuu]

Hi Brando! I have no idea about classical SMT/ATP solvers, would you name some of them?

[brando90]

Of course! CVC5, Vampire, Z3 and I bet many more! I don't know what format of theorems they take but I'm guessing they are FOL. I hope to find out more and help with this issue eventually :) Get Outlook for Android<https://aka.ms/AAb9ysg>

…

________________________________ From: Kunhao ZHENG ***@***.***> Sent: Tuesday, November 1, 2022 8:18:44 PM To: openai/miniF2F ***@***.***> Cc: Brando Miranda ***@***.***>; Author ***@***.***> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122) Hi Brando! I have no idea about classical SMT/ATP solvers, would you name some of them? — Reply to this email directly, view it on GitHub<#122 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAOE6LWS4Z7D4BRXN3QHQ5DWGHMRJANCNFSM6AAAAAARTXFK4M>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[brando90]

If you run Isabelle's sledgehammer or coqhammer they usually say which atp they are running in your current open goals. Get Outlook for Android<https://aka.ms/AAb9ysg>

…

________________________________ From: Brando Miranda ***@***.***> Sent: Tuesday, November 1, 2022 10:25:47 PM To: openai/miniF2F ***@***.***>; openai/miniF2F ***@***.***> Cc: Author ***@***.***> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122) Of course! CVC5, Vampire, Z3 and I bet many more! I don't know what format of theorems they take but I'm guessing they are FOL. I hope to find out more and help with this issue eventually :) Get Outlook for Android<https://aka.ms/AAb9ysg>

________________________________ From: Kunhao ZHENG ***@***.***> Sent: Tuesday, November 1, 2022 8:18:44 PM To: openai/miniF2F ***@***.***> Cc: Brando Miranda ***@***.***>; Author ***@***.***> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122) Hi Brando! I have no idea about classical SMT/ATP solvers, would you name some of them? — Reply to this email directly, view it on GitHub<#122 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAOE6LWS4Z7D4BRXN3QHQ5DWGHMRJANCNFSM6AAAAAARTXFK4M>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[DyeKuu]

as far as i know there is no undergoing efforts on porting minif2f to these solvers. would like to know if this is in principle feasible?

[brando90]

Would love to know if this is feasible for sue. Do you know? I will ask my circle of connections. Get Outlook for Android<https://aka.ms/AAb9ysg>

…

________________________________ From: Kunhao ZHENG ***@***.***> Sent: Wednesday, November 2, 2022 7:02:47 PM To: openai/miniF2F ***@***.***> Cc: Brando Miranda ***@***.***>; Author ***@***.***> Subject: Re: [openai/miniF2F] FOL/SMT classical tools support? (Issue #122) as far as i know there is no undergoing efforts on porting minif2f to these solvers. would like to know if this is in principle feasible? — Reply to this email directly, view it on GitHub<#122 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAOE6LV3LHVQJCQF3GCALXDWGMMMPANCNFSM6AAAAAARTXFK4M>. You are receiving this because you authored the thread.Message ID: ***@***.***>