New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
symbols (+, -) in comments and axioms #29
Comments
I guess this is an issue about what characters are acceptable as function and predicate names. We should be more explicit about it. I don't think "+" and "-" are translated correctly to TPTP either. |
@thahmann I brought this up with Michael last week since the lab might move towards using Vampire (at least for building models for the larger ontologies like FOUnt), and he mentioned to me that we cannot change the relation/function/constant names for the PSL theories that use "inf+" and "inf-" due to the ISO standard (unless revisions to the standard are made). When translated into TPTP, Vampire throws an error for me since + and - aren't recognized as variables. Perhaps we can just use symbols.conf as a way to rename them when macleod does the translation of the ontologies that use inf- and inf+ (like "infNeg" or "infPos")? It would probably be the easiest approach. |
Yes, that is exactly what I meant. We can have these operations in Clif files but translate them to something else in the translations to TPTP and Prover9 using the symbols.conf. Btw, does Vampire construct larger models? Or did you mean TPTP model finders (e.g. Paradox)? |
Oh I meant Paradox for model finding and Vampire for theorem proving. We might end up using both in place of Prover9 -- I'm not too sure what Michael has decided on yet since neither of us like looking at the TPTP syntax... but Prover9 becomes crippled when we deal with the newer and bigger ontologies in COLORE (e.g., some of newer the tripartite_incidence theories). p.s. Did you test the newer version of Vampire with Macleod? The very old vampire_mac file works fine and prints out proofs in the *.vam.out. files, but the current version (4.2.2) does not print anything in the output files when I configure it with Macleod. |
With the Python3 version of Macleod, the GUI output is somewhat misleading when dealing with symbols like + or - in both the Common Logic comments and axioms.
For example, opening http://colore.oor.net/psl_core/psl_core.clif will trigger the following output in the latest version of Macleod:
This doesn't affect the translation into LADR or TPTP but the output in the GUI is misleading.
In comparison, with the Python2 version of macleod, this error message doesn't appear in the GUI output:
This only affects the following CLIF files:
The text was updated successfully, but these errors were encountered: