Running solvers on TPTP + converting kernel proofs to Lisa code #208
Conversation
augustepoiroux
force-pushed
the
kernel2tactic
branch
from
bac2e92 to
81fb6da
Compare
| def mkString(args: Seq[Formula]): String = if (args.length == 2) (args(0).toString() + " " + toString() + " " + args(1).toString()) else toString() + "(" + args.mkString(", ") + ")" | ||
| def mkString(args: Seq[Formula]): String = if (args.length == 1) { | ||
| underlyingLabel match | ||
| case K.Neg => toString() + "(" + args(0).toString() + ")" |
There was a problem hiding this comment.
Why this change? I think if label is K.Neg then it prints the same result, but we lose the infix notation if args.length == 2 ? Also the representation is not injective because and(A) will be printed as A
There was a problem hiding this comment.
I did these changes to get printed results as close as possible to actual Lisa code.
- When we only have one argument, and(A) is not accepted by the parser, so that's why I'm printing A instead. And Neg is a special case to handle here.
- I think infix notation was not always accepted by Lisa parser, that's why for args.length > 1 I'm printing everything using (A and B and C)-like notation
If this is not the appropriate place to do this, or if the main purpose of this string representation is not to be as close as possible to Lisa code, tell me where I should put this :)
There was a problem hiding this comment.
Which parser do you mean? Scala compiler or the FOL parser? If the last one, we're not using it and it anywhere and it has multiple other differences. If the first one, if it doesn't accept and(A) it can be made to accept e.g. and.multi(A).
But printing A instead of and(A) is not correct
| case n: N => ConstantPredicateLabel(cpl.id, cpl.arity.asInstanceOf) | ||
| case n: N => | ||
| if (cpl.id == Identifier("=")) | ||
| ConstantPredicateLabel.infix("===", cpl.arity.asInstanceOf) |
There was a problem hiding this comment.
This doesn't seem correct, because asFrontLabel(K.equals).underlying != K.equals, which is a problem.
Probably you want to change just the pretty printing of symbols whose identifier is "=".
For example, override the toString method of the equality symbol in lisa.utils
There was a problem hiding this comment.
Oh I see, I did this here because I didn't find somewhere else to do it. I will try to do that in lisa.utils then 👍
This pull request adds the following files:
lisa-utils:ProofsConverter.scala: methods to transform kernel proofs to Lisa code proofsRunSolver.scala: a class to run a solver for a given timelisa-examples:Kernel2Code.scala: showcases examples of kernel proofs conversion to Lisa code proofs.TPTPSolver.scala: extract, try to solve TPTP problems, and export LIsa code proofs of solved problems in a JSON file.A few files in
lisa-utilsare modified to improve the string conversion correctness:Common.scala,FOLHelpers.scala,Sequents.scalaTPTP parser script is also updated to handle edge cases:
KernelParser.scala