2020-03-26 17:3:56 (GMT)
"Lazy clausification for FOOL" - does that describe what you would like to do?
2020-03-26 17:16:28 (GMT)
Wait
2020-03-26 17:17:2 (GMT)
What we want in the end is complete support for booleans natively in the logic.
2020-03-26 17:17:13 (GMT)
It does not have to be FOOL-based.
2020-03-26 17:17:57 (GMT)
Maybe we realize that we do not have to pull out any boolean terms like FOOL but lazy clausification together with boolean extensionality rules are enough
2020-03-26 17:17:59 (GMT)
Ok, maybe a bad name. I mean the FOOL logic, not the method.
2020-03-26 17:18:37 (GMT)
You had Superposition with Lambdas paper
2020-03-26 17:18:53 (GMT)
now this one could be named Superposition with nested Booleans
2020-03-26 17:20:3 (GMT)
or only Booleans
2020-03-26 18:2:48 (GMT)
What's going to be the different with "the vampire and the fool"?
2020-03-26 18:4:52 (GMT)
Ahmed, congrats on all three papers being accepted !!!
2020-03-26 18:7:7 (GMT)
sorry Simon
2020-03-26 18:7:10 (GMT)
wrong chat :)
2020-03-26 18:7:59 (GMT)
fyi I tend to stay in the main view ("all messages")
2020-03-26 18:8:11 (GMT)
let me answer your question: many things. First of all, there is going to be no preprocessing, but everything will be done natively. Second, we will use lazy clausification and maybe do away with the rule Fool Paramodulation
2020-03-26 18:8:37 (GMT)
Simon Cruanes said:
fyi I tend to stay in the main view ("all messages")
Indeed, this is easier to control :)
2020-03-26 18:26:37 (GMT)
I think what Petar forgot to mention is that there would be a refutational completeness result.
2020-03-26 18:26:49 (GMT)
We're really talking about "Superposition for FOOL" here.
2020-03-26 18:27:11 (GMT)
Or "Superposition for Full First-Order Logic with Interpreted Booleans" if we want to be precise.
2020-03-26 18:27:22 (GMT)
(It's not just TPTP/FOOL but also SMT-LIB.)
2020-03-26 18:27:58 (GMT)
It appears to be a necessary stepping stone towards Superposition for Full HOL (part 3 of 3 of the Bentkamp trilogy).
2020-03-26 19:10:13 (GMT)
I am not sure if they state this explicitly in the paper, but I think the original FOOL method is also refutationally complete.
2020-03-26 19:38:0 (GMT)
They have the model preservation theorem.
2020-03-26 19:38:36 (GMT)
In my understanding, this amounts to completenes -- because if original formula did not have models, then the translated one will not and you will be able to derive empty clause for the translation