2020-06-29 7:7:59 (GMT)
This thread is to discuss about the talks presented in the 2nd session of PAAR 2020:
2020-06-29 9:48:55 (GMT)
All papers are available on the web page: http://paar2020.gforge.inria.fr/
2020-06-29 13:58:39 (GMT)
Session 2 is about to start!
2020-06-29 14:55:49 (GMT)
We have an open question in this session, relative to the second talk's future work: Is fluted logic decidable at all?
2020-06-29 15:1:6 (GMT)
I found a paper related to the decidability of fluted logic (from Renate). Apparently it is decidable (@Hans de Nivelle ) : https://link.springer.com/chapter/10.1007/10721959_34
2020-06-29 15:52:52 (GMT)
Concerning Simon's comment, wrongly posted in session 1. I believe it is already the case that CASC (and TPTP library) use restricted subsets of the TPTP syntax. Geoff is trying not to place too much a burden on the parsers. But the subsets are not documented as far as I know.
2020-06-29 15:54:53 (GMT)
Well if CASC used the whole TPTP syntax it would need to have a "syntax" category, where the winner is the prover that successfully parses the most problems :stuck_out_tongue_wink:
2020-06-29 15:55:25 (GMT)
More seriously, a reference parser for subsets of TPTP (including the subsets used in CASC) would be great.
2020-06-29 15:57:13 (GMT)
Wouldn't we also need a "not-syntax" category where the winner is the prover who successfully identifies that the problems are syntactically incorrect.... I've already got a couple of print statements that will do very well in both categories :)
2020-06-29 15:57:48 (GMT)
The winner is the one that submits the smallest possible patch to the EBNF that makes the problem syntactically valid.