2020-01-25 18:4:6 (GMT)
My understanding was that Zipperposition is polymorphic, but when I run on any polymorphic problems in the TPTP library, it returns inappropriate. Is this just because the parser needs to be updated to handle TPTP sytax?
2020-01-25 18:47:10 (GMT)
How do you mean exactly "inappropriate"? Like, it refuses to parse?
2020-01-25 21:2:42 (GMT)
https://sneeuwbal.zulipchat.com/#narrow/stream/192467-zipperposition/topic/benchpress.3A.20benchmarking.20tool/near/186584421 seems like Petar replied to the wrong conversation :p
2020-03-10 16:29:35 (GMT)
Simon Cruanes said:
https://sneeuwbal.zulipchat.com/#narrow/stream/192467-zipperposition/topic/benchpress.3A.20benchmarking.20tool/near/186584421 seems like Petar replied to the wrong conversation :p
Are there any references explaining how polymorphism has been implemented in Zipperposition?
2020-03-10 16:33:35 (GMT)
You can find some information in my thesis (chap 3). Mostly it's explicit polymorphism (polymorphic symbols take type arguments, like = α t u if t : α).