symbols (+, -) in comments and axioms

[carmenchui]

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:

• http://colore.oor.net/psl_core/psl_core.clif
• http://colore.oor.net/psl_core/psl_core_root.clif
• and possibly any other CLIF files that have symbols in their constants

[thahmann]

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.
There is an approach using a symbol table (symbols.conf) to specify how certain special symbols are translated (used successfully with CODI ontologies, where < and <= were used and replaced by lt and leq). Maybe this replacement should happen as part of the new object structure as well.

[carmenchui]

@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.

[thahmann]

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. We should just take the symbols.conf into account when parsing Clif files for the editor -- which is the part that is missing right now.

Btw, does Vampire construct larger models? Or did you mean TPTP model finders (e.g. Paradox)?

[carmenchui]

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.