Skip to content

Commit

Permalink
Many changes to tidy up use of TFF labels and pass LEO-III-STC checks
Browse files Browse the repository at this point in the history 
Signed-off-by: apease <apease@articulatesoftware.com>
  • Loading branch information
@apease
apease committed Feb 3, 2025
1 parent 85d1ef6 commit 0115d2d
Show file tree
Hide file tree
Showing 4 changed files with 106 additions and 34 deletions.
10 changes: 10 additions & 0 deletions src/java/com/articulate/sigma/Formula.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2612,6 +2612,16 @@ public static boolean isComparisonOperator(String term) {
return (!StringUtil.emptyString(term) && COMPARISON_OPERATORS.contains(term));
}

/** ***************************************************************
* Returns true if term is a SUO-KIF inequality, else returns false.
*
* @param term A String.
*/
public static boolean isInequality(String term) {

return (!StringUtil.emptyString(term) && INEQUALITIES.contains(term));
}

/** ***************************************************************
* Returns true if term is a SUO-KIF mathematical function, else
* returns false.
Expand Down
72 changes: 51 additions & 21 deletions src/java/com/articulate/sigma/trans/SUMOKBtoTFAKB.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ public class SUMOKBtoTFAKB extends SUMOKBtoTPTPKB {

public static boolean initialized = false;

public static boolean debug = false;
public static boolean debug = true;

public static Set<String> qChildren = new HashSet<>();
public static Set<String> iChildren = new HashSet<>();
Expand Down Expand Up @@ -220,20 +220,38 @@ public static String translateName(String s) {
*/
public void writeSort(String t, PrintWriter pw) {

String label = translateName(t) + "_sig";
String label;
label = translateName(t) + "_sig";
pw.println("% writeSort(): term: " + t);
String bareTerm = SUMOtoTFAform.getBareTerm(t);
pw.println("% bare term: " + bareTerm);
if (sortLabels.contains(label)) {
pw.println("% duplicate label " + label + " for " + t);
return;
}
else {
pw.println("% add label " + label);
pw.println("% add label (writeSort) " + label);
sortLabels.add(label);
}
String output = "tff(" + label + ",type,s__" + t;
if (Formula.isLogicalOperator(SUMOtoTFAform.getBareTerm(t)) ||
SUMOtoTFAform.getBareTerm(t).equals("equal") ||
kb.isRelation(SUMOtoTFAform.getBareTerm(t)))
output = output + "__m";
String output;
if (Formula.isInequality(bareTerm))
t = translateName(t);
if (!t.startsWith(Formula.termSymbolPrefix))
t = Formula.termSymbolPrefix + t;
output = "tff(" + label + ",type," + t;
//if (Formula.isLogicalOperator(bareTerm) ||
if (kb.isRelation(bareTerm) ||
bareTerm.equals("equal")) {
// ||
// (kb.isRelation(bareTerm) && !Formula.isMathFunction(bareTerm))) {
// && !Formula.isInequality(bareTerm))) {
pw.println("% logop: " + Formula.isLogicalOperator(bareTerm));
pw.println("% is relation: " + kb.isRelation(bareTerm));
pw.println("% is inequality: " + Formula.isInequality(bareTerm));
pw.println("% is math: " + Formula.isMathFunction(bareTerm));
if (!output.endsWith(Formula.termMentionSuffix))
output = output + Formula.termMentionSuffix;
}
output = output + " : $i ).";
pw.println(output);
}
Expand All @@ -257,11 +275,16 @@ public int getVariableAritySuffix(String t) {
*/
public void writeRelationSort(String t, PrintWriter pw) {

if (debug) System.out.println("SUMOKBtoTFAKB.writeRelationSort(): " + t);
pw.println("% SUMOKBtoTFAKB.writeRelationSort(): " + t);
if (t.endsWith("Fn") != kb.isFunction(t))
System.out.println("ERROR in writeRelationSort(): is function mismatch with term name : " + t + ", " + kb.isFunction(t));
if (Formula.isLogicalOperator(t) || Formula.isMathFunction(t))
if (Formula.isLogicalOperator(t) || Formula.isMathFunction(t) || Formula.isComparisonOperator(t)) {
String label = translateName(t);
String output = "tff(" + label + ",type," + label +
" : $i ).";
pw.println(output);
return;
}
List<String> sig = kb.kbCache.signatures.get(t);
int endIndex = sig.size();
if (KButilities.isVariableArity(kb,SUMOtoTFAform.withoutSuffix(t)))
Expand Down Expand Up @@ -289,6 +312,10 @@ public void writeRelationSort(String t, PrintWriter pw) {
if (sigBuf.length() == 0) {
pw.println("% Error in SUMOKBtoTFAKB.writeRelationSort(): " + t);
pw.println("% Error in SUMOKBtoTFAKB.writeRelationSort(): signature: " + sig);
String label = translateName(t);
String output = "tff(" + label + ",type," + label +
" : $i ).";
pw.println(output);
pw.flush();
return;
//Thread.dumpStack();
Expand All @@ -299,15 +326,15 @@ public void writeRelationSort(String t, PrintWriter pw) {
relname = relname.substring(0,relname.length()-3);
String range = sig.get(0);
String label = translateName(t);
if (label.endsWith("_m"))
if (label.endsWith(Formula.termMentionSuffix))
label = label.substring(0,label.length()-2);
label = label + "_sig_rel";
if (sortLabels.contains(label)) {
pw.println("% duplicate label " + label + " for " + relname);
return;
}
else {
pw.println("% add label " + label);
pw.println("% add label (relation sort) " + label);
sortLabels.add(label);
}
if (kb.isFunction(t)) {
Expand All @@ -320,7 +347,7 @@ public void writeRelationSort(String t, PrintWriter pw) {
" : ( " + sigStr + " ) > $o ).";
pw.println(output);
}
String output = "tff(" + label + "_m,type," + relname + "_m" +
String output = "tff(" + label + Formula.termMentionSuffix + ",type," + relname + Formula.termMentionSuffix +
" : $i ).";
pw.println(output);
}
Expand Down Expand Up @@ -589,16 +616,18 @@ public void writeSorts(PrintWriter pw) {
handleListFn(toExtend);
String fnSuffix;
for (String t : kb.getTerms()) {
String bareTerm = SUMOtoTFAform.getBareTerm(t);
pw.println("% SUMOKBtoTFAKB.writeSorts(): " + t);
if (debug) System.out.println("SUMOKBtoTFAKB.writeSorts(): " + t);
if (debug) System.out.println("SUMOKBtoTFAKB.writeSorts(): t: " + t);
if (debug) System.out.println("SUMOKBtoTFAKB.writeSorts(): bareTerm: " + bareTerm);
if (debug) System.out.println("kb.isRelation(t) " + kb.isRelation(t));
if (debug) System.out.println("!alreadyExtended(t): " + !alreadyExtended(t));
if (debug) System.out.println("!Formula.isComparisonOperator(t)): " + !Formula.isComparisonOperator(t));
if (debug) System.out.println("!Formula.isMathFunction(t)): " + !Formula.isMathFunction(t));
if (!Character.isLetter(t.charAt(0)) || Formula.isTrueFalse(t))
continue;
if (kb.isFunction(t)) {
if (Formula.isLogicalOperator(t) || t.equals("equal") ) {
if (kb.isFunction(bareTerm)) {
if (Formula.isLogicalOperator(bareTerm) || t.equals("equal") ) {
continue;
}
else {
Expand All @@ -607,9 +636,9 @@ public void writeSorts(PrintWriter pw) {
processRelationSort(toExtend, t);
}
}
else if (kb.isRelation(t) && !alreadyExtended(t) && !t.equals("ListFn")
&& !Formula.isComparisonOperator(t) && !Formula.isMathFunction(t)) {
if (hasNumericSuperArg(t) || listOperator(t)) {
else if (kb.isRelation(bareTerm) && !alreadyExtended(t) && !bareTerm.equals("ListFn")
&& !Formula.isComparisonOperator(bareTerm) && !Formula.isMathFunction(bareTerm)) {
if (hasNumericSuperArg(bareTerm) || listOperator(bareTerm)) {
writeRelationSort(t, pw);
processRelationSort(toExtend, t);
}
Expand All @@ -623,9 +652,10 @@ else if (kb.isRelation(t) && !alreadyExtended(t) && !t.equals("ListFn")
String sep, newTerm;
pw.println("% SUMOKBtoTFAKB.writeSorts(): starting on toExtend sorts");
for (String k : toExtend.keySet()) {
vals = toExtend.get(k);
String bareTerm = SUMOtoTFAform.getBareTerm(k);
vals = toExtend.get(bareTerm);
fnSuffix = "";
if (kb.isFunction(k) || k.endsWith("Fn")) // variable arity functions with numerical suffixes not in kb yet
if (kb.isFunction(bareTerm) || bareTerm.endsWith("Fn")) // variable arity functions with numerical suffixes not in kb yet
fnSuffix = "Fn";
for (String e : vals) {
kb.kbCache.extendInstance(k, e + fnSuffix);
Expand Down
28 changes: 21 additions & 7 deletions src/java/com/articulate/sigma/trans/SUMOformulaToTPTPformula.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,46 +133,60 @@ private static String translateWord_1(String st, int type, boolean hasArguments)
char ch1 = ((st.length() > 1)
? st.charAt(1)
: 'x');
if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): here1: ");
if (ch0 == '?' || ch0 == '@')
return(Formula.termVariablePrefix + st.substring(1).replace('-','_'));

if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): here2: ");
//----Translate special predicates
if (lang.equals("tff")) {
if (Formula.isInequality(st) && !hasArguments)
return Formula.termSymbolPrefix + st + Formula.termMentionSuffix;
translateIndex = kifPredicates.indexOf(st);
if (translateIndex != -1)
return (tptpPredicates.get(translateIndex) + (hasArguments ? "" : mentionSuffix));
}
if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): here3: ");
//----Translate special constants
translateIndex = kifConstants.indexOf(st);
if (translateIndex != -1)
return(tptpConstants.get(translateIndex) + (hasArguments ? "" : mentionSuffix));
if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): here4: ");
//----Translate special functions
if (lang.equals("tff")) {
translateIndex = kifFunctions.indexOf(st);
if (translateIndex != -1)
return (tptpFunctions.get(translateIndex) + (hasArguments ? "" : mentionSuffix));
}
if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): here5: ");
//----Translate operators
translateIndex = kifOps.indexOf(st);
if (translateIndex != -1 && hasArguments) {
return (tptpOps.get(translateIndex));
}
if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): here6: ");
//----Do nothing to numbers
if (type == StreamTokenizer.TT_NUMBER ||
(st != null && (Character.isDigit(ch0) ||
(ch0 == '-' && Character.isDigit(ch1))))) {
return(st);
}
String term = st;

if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): here7: ");
if (!hasArguments) {
if ((!term.endsWith(mentionSuffix) && Character.isLowerCase(ch0))
|| term.endsWith("Fn")
|| KB.isRelationInAnyKB(term)) {
term += mentionSuffix;
if (debug) System.out.println("INFO in SUMOformulaToTPTPformula.translateWord_1(): no arguments: " + term);
if (!Formula.isInequality(term)) {
if ((!term.endsWith(mentionSuffix) && Character.isLowerCase(ch0))
|| term.endsWith("Fn")
|| KB.isRelationInAnyKB(term)) {
term += mentionSuffix;
}
}
else {
return (Formula.termSymbolPrefix + st.substring(1).replace('-','_'));
}

}
if (kifOps.contains(term))
if (kifOps.contains(term) && hasArguments)
return(term);
else
return(Formula.termSymbolPrefix + term);
Expand Down
30 changes: 24 additions & 6 deletions src/java/com/articulate/sigma/trans/SUMOtoTFAform.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -838,10 +838,11 @@ else if (op.startsWith("lessThan"))
public static String getBareTerm(String s) {

String result = s;
result = result.replaceFirst(Formula.termSymbolPrefix, "");
Pattern p = Pattern.compile("(.*)__.*");
if (result.startsWith(Formula.termSymbolPrefix))
result = result.substring(3);
Pattern p = Pattern.compile("^(.+)__.*");
Matcher m = p.matcher(result);
while (m.matches()) {
while (m.lookingAt()) {
result = m.group(1);
m = p.matcher(result);
}
Expand Down Expand Up @@ -1183,10 +1184,14 @@ public static String processRecurse(Formula f, String parentType) {
if (Character.isDigit(ttype))
ttype = StreamTokenizer_s.TT_NUMBER;
String promotion = numTypePromotion(f,parentType);
String result = null;
if (debug) System.out.println("SUMOtoTFAform.processRecurse(): promotion: " + promotion);
if (promotion != null)
return promotion + SUMOformulaToTPTPformula.translateWord(f.getFormula(),ttype,false) + ")";
result = promotion + SUMOformulaToTPTPformula.translateWord(f.getFormula(),ttype,false) + ")";
else
return SUMOformulaToTPTPformula.translateWord(f.getFormula(),ttype,false);
result = SUMOformulaToTPTPformula.translateWord(f.getFormula(),ttype,false);
if (debug) System.out.println("SUMOtoTFAform.processRecurse(): result: " + result);
return result;
}
Formula car = f.carAsFormula();
String op = car.getFormula();
Expand Down Expand Up @@ -2391,14 +2396,23 @@ public static String process(Formula f, boolean query) {
*/
public static String process(String s, boolean query) {

if (s.startsWith("(domain greaterThan")) {
SUMOtoTFAform.debug = true;
SUMOformulaToTPTPformula.debug = true;
}
filterMessage = "";
if (s.contains("ListFn"))
filterMessage = "SUMOtoTFAform.process(): Formula contains a list operator";
//if (StringUtil.emptyString(s) || numConstAxioms.contains(s))
if (StringUtil.emptyString(s)) // || numConstAxioms.contains(s))
return "";
Formula f = new Formula(s);
return process(f,query);
String res = process(f,query);
if (s.startsWith("(domain greaterThan")) {
SUMOtoTFAform.debug = false;
SUMOformulaToTPTPformula.debug = false;
}
return res;
}

/** *************************************************************
Expand Down Expand Up @@ -2862,6 +2876,7 @@ else if (args != null && args.length > 0 && args[0].equals("-h"))
}
else if (args != null && args.length > 1 && args[0].equals("-f")) {
debug = true;
SUMOformulaToTPTPformula.debug = true;
Formula f = new Formula(args[1]);
System.out.println("in TFA: " + process(f,false));
}
Expand All @@ -2870,6 +2885,9 @@ else if (args != null && args.length > 0 && args[0].equals("-t")) {
System.out.println(bare);
KB kb = KBmanager.getMgr().getKB("SUMO");
System.out.println(kb.isRelation(bare));
bare = getBareTerm("refers__1En2In");
System.out.println(bare);
System.out.println(kb.isRelation(bare));
/**
if (debug) System.out.println("SUMOtoTFAform.main(): contains ListFn__1Fn: " + kb.terms.contains("ListFn__1Fn"));
String kbName = KBmanager.getMgr().getPref("sumokbname");
Expand Down

0 comments on commit 0115d2d

Please sign in to comment.