com.articulate.sigma.trans

Class THF

java.lang.Object

com.articulate.sigma.trans.THF

public class THF
extends java.lang.Object

This class handles the conversion of problems (= axioms + queries) from their KIF representation into a THF representation; THF is the TPTP standard for classical higher-order logic, i.e. Church's simple theory. The main function provided is KIF2THF(KIFaxioms,KIFqueries,KnowledgeBase) A challenge part in this transformation is the computation of an appropriate typing for the KIF terms and formulas. This is partly non-trivial. The conversion is intented to work purely syntactically (when no typing-relevant information from SUMO is available) or mixed syntactically-semantically (when typing-relevant information from SUMO is available). A small example: The KIF Problem with axioms (holdsDuring (YearFN n2009) (enjoys Mary Cooking)) (holdsDuring (YearFN n2009) (=> (instance ?X Female) (wants Ben ?X))) (holdsDuring ?X (instance Mary Female)) and Query (holdsDuring ?X (and (?Y Mary Cooking) (wants ?Z Mary))) is tranlated into the THF problem: %%% The extracted Signature %%% thf(holdsDuring,type,(holdsDuring: ($i>$o>$o))). thf(enjoys_THFTYPE_IiioI,type,(enjoys_THFTYPE_IiioI: ($i>$i>$o))). thf(female,type,(female: $i)). thf(n2009,type,(n2009: $i)). thf(cooking,type,(cooking: $i)). thf(ben,type,(ben: $i)). thf(yearFN_THFTYPE_IiiI,type,(yearFN_THFTYPE_IiiI: ($i>$i))). thf(mary,type,(mary: $i)). thf(wants,type,(wants: ($i>$i>$o))). thf(instance_THFTYPE_IiioI,type,(instance_THFTYPE_IiioI: ($i>$i>$o))). %%% The translated axioms %%% thf(ax,axiom,((! [X: $i]: (holdsDuring @ X @ (instance_THFTYPE_IiioI @ mary @ female))))). thf(ax,axiom,((! [X: $i]: (holdsDuring @ (yearFN_THFTYPE_IiiI @ n2009) @ ((instance_THFTYPE_IiioI @ X @ female) => (wants @ ben @ X)))))). thf(ax,axiom,((holdsDuring @ (yearFN_THFTYPE_IiiI @ n2009) @ (enjoys_THFTYPE_IiioI @ mary @ cooking)))). %%% The translated conjectures %%% thf(con,conjecture,((? [X: $i,Y: $i,Z: $i]: (holdsDuring @ X @ ((enjoys_THFTYPE_IiioI @ mary @ Y) & (wants @ Z @ mary)))))). This THF problem can be solved effectively by TPTP THF compliant higher-order theorem provers. The transformation often needs to introduce several 'copies' of KIF constants for different THF types. Therefore some constant symbols become tagged with type information during the transformation process. Example for tagged contant symbols above enjoys_THFTYPE_IiioI and instance_THFTYPE_IiioI.

Constructor Summary

Constructors

Constructor and Description
THF()

Method Summary

Modifier and Type	Method and Description
java.lang.String	KIF2THF(java.util.Collection<Formula> axiomsC, java.util.Collection<Formula> conjecturesC, KB kb) public String KIF2THF(Collection axioms, Collection conjectures, KB kb) { // string builders for the essential results of the translation: // signature, axioms, and conjectures StringBuilder signatureResult = new StringBuilder(); signatureResult.append("\n%%% The extracted Signature %%%"); StringBuilder axiomsResult = new StringBuilder(); axiomsResult.append("\n\n%%% The translated axioms %%%"); StringBuilder conjecturesResult = new StringBuilder(); conjecturesResult.append("\n\n%%% The translated conjectures %%%"); // tags and a map to distinguish axioms from conjectures String axTag = "ax"; String conTag = "con"; HashMap taggedFormulas = new HashMap(); for (Iterator iter = axioms.iterator(); iter.hasNext();) { Formula ax = (Formula) iter.next(); taggedFormulas.put(ax,axTag); } for (Iterator iter = conjectures.iterator(); iter.hasNext();) { Formula con = (Formula) iter.next(); taggedFormulas.put(con,conTag); } // the main loop; we proceed formula by formula and work with side effects // to variables introduced above (I know that this is terrible programming style!) for (Iterator iter = taggedFormulas.keySet().iterator(); iter.hasNext();) { Formula form = (Formula) iter.next(); // formula f contains the explicitly quantified formula under // consideration, the quantifier (universal/existential) is // determined correctly for axioms and conjectures Formula f = new Formula(); if (taggedFormulas.get(form).equals(axTag)) { f.read(form.makeQuantifiersExplicit(false)); } else if (taggedFormulas.get(form).equals(conTag)) { f.read(form.makeQuantifiersExplicit(true)); } System.out.println("\nKIF2THF -- translating KIF formula: " + f.theFormula.trim()); // we request some semantic type-relevant information on the function and // relation symbols involved; this information is used with priority below HashMap relTypeInfo = f.gatherRelationsWithArgTypes(kb); // we initialize the terms-to-types mapping and start the actual translation terms = new HashMap(); String res = toTHF1(f,boolTp,relTypeInfo); // toTHF1 may return a THF translation that still contains many occurences // of the (kind of) polymorphic 'unkownTp' and in this case we apply further // translation attempts employing the incrementially refined term-to-type // information.
static void	main(java.lang.String[] args) A test method.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

THF

public THF()

Method Detail

KIF2THF

public java.lang.String KIF2THF(java.util.Collection<Formula> axiomsC,
                                java.util.Collection<Formula> conjecturesC,
                                KB kb)

public String KIF2THF(Collection axioms, Collection conjectures, KB kb) { // string builders for the essential results of the translation: // signature, axioms, and conjectures StringBuilder signatureResult = new StringBuilder(); signatureResult.append("\n%%% The extracted Signature %%%"); StringBuilder axiomsResult = new StringBuilder(); axiomsResult.append("\n\n%%% The translated axioms %%%"); StringBuilder conjecturesResult = new StringBuilder(); conjecturesResult.append("\n\n%%% The translated conjectures %%%"); // tags and a map to distinguish axioms from conjectures String axTag = "ax"; String conTag = "con"; HashMap taggedFormulas = new HashMap(); for (Iterator iter = axioms.iterator(); iter.hasNext();) { Formula ax = (Formula) iter.next(); taggedFormulas.put(ax,axTag); } for (Iterator iter = conjectures.iterator(); iter.hasNext();) { Formula con = (Formula) iter.next(); taggedFormulas.put(con,conTag); } // the main loop; we proceed formula by formula and work with side effects // to variables introduced above (I know that this is terrible programming style!) for (Iterator iter = taggedFormulas.keySet().iterator(); iter.hasNext();) { Formula form = (Formula) iter.next(); // formula f contains the explicitly quantified formula under // consideration, the quantifier (universal/existential) is // determined correctly for axioms and conjectures Formula f = new Formula(); if (taggedFormulas.get(form).equals(axTag)) { f.read(form.makeQuantifiersExplicit(false)); } else if (taggedFormulas.get(form).equals(conTag)) { f.read(form.makeQuantifiersExplicit(true)); } System.out.println("\nKIF2THF -- translating KIF formula: " + f.theFormula.trim()); // we request some semantic type-relevant information on the function and // relation symbols involved; this information is used with priority below HashMap relTypeInfo = f.gatherRelationsWithArgTypes(kb); // we initialize the terms-to-types mapping and start the actual translation terms = new HashMap(); String res = toTHF1(f,boolTp,relTypeInfo); // toTHF1 may return a THF translation that still contains many occurences // of the (kind of) polymorphic 'unkownTp' and in this case we apply further // translation attempts employing the incrementially refined term-to-type // information. This is done via repetitive calls to toTHF2. This loop // terminates when the signature localsig, which is storing the latest constant-to-symbols // mapping, is free of occurences of the 'unknownTp'. // toTHF2 always starts a fresh translation attempt for the KIF formula stored in // variable kifFormula, which may itself be modified by renamings of symbols. // It is thus important in the code to maintain a correspondence between the symbols in // this kifFormula, the terms-to-type mappings, and the incrementially refined THF // translation; the handling of e.g. the different upper and lower case conventions // between KIF and TPTP THF further complicates matters. This issue makes the code // particularly fragile, also since it exploits string processing way to much. HashMap oldsig = new HashMap(); kifFormula = new StringBuilder(); while (containsUnknownTp(localsig)) { if (!oldsig.equals(localsig)) { THFdebugOut("\n Debug: Enter new regular topmost call to THF2"); oldsig = (HashMap) localsig.clone(); res = toTHF2(f); f = new Formula(); f.read(kifFormula.toString()); kifFormula = new StringBuilder(); localsig = clearMapFor(localsig,f.theFormula.trim()); subst = clearMapFor(subst,f.theFormula.trim()); } else { THFdebugOut("\n Debug: Enter new topmost call to THF2 with constant symbol substitution"); oldsig = (HashMap) localsig.clone(); Set keyset = subst.keySet(); THFdebugOut(" Debug: f before is " + f.toString()); THFdebugOut(" Debug: subst is " + subst.toString()); String fsubst = f.toString(); for (Iterator it = keyset.iterator(); it.hasNext();) { String key = (String) it.next(); String keysubst = (String) subst.get(key); THFdebugOut("\n Debug: fsubst before is " + fsubst); THFdebugOut(" Debug: key is " + key + " and keysubst is " + keysubst); fsubst = applySubstTo(key,keysubst,fsubst); THFdebugOut(" Debug: fsubst after is " + fsubst); } f = new Formula(); f.read(fsubst); THFdebugOut("\n Debug: f after is " + f.toString()); res = toTHF2(f); f = new Formula(); f.read(kifFormula.toString()); kifFormula = new StringBuilder(); localsig = clearMapFor(localsig,f.theFormula.trim()); subst = clearMapFor(subst,f.theFormula.trim()); } } // this final one-more call to toTHF2 seems not needed anymore // but is was in earlier versions. // if (res.contains(unknownTp)) { // THFdebugOut("\n Debug: Enter one more topmost call to THF2"); res = toTHF2(f); // } // now we can add the computed THF translation for // formula f to the appropriate result string builder if (taggedFormulas.get(form).equals(axTag)) { String resAx = ""; if (res.startsWith("%")) { resAx = "\n" + res; } else { resAx = "\n thf(ax,axiom,(" + res + "))."; } System.out.println("KIF2THF -- result: " + resAx); axiomsResult.append(resAx); } else if (taggedFormulas.get(form).equals(conTag)) { String resCon = ""; if (res.startsWith("%")) { resCon = "\n" + res; } else { resCon = "\n thf(con,conjecture,(" + res + "))."; } System.out.println("KIF2THF -- result: " + resCon); conjecturesResult.append(resCon); } else { axiomsResult.append("\n something went wrong for " + form + " " + res); } overallsig.putAll(localsig); localsig = new HashMap(); } // After the translation processed has terminated for all formulas f, we read off // the THF signature from the map 'overallsig' Set constants = overallsig.keySet(); for (Iterator it = constants.iterator(); it.hasNext();) { String con = (String) it.next(); String ty = (String) overallsig.get(con); signatureResult.append("\n thf(" + con + ",type,(" + con + ": " + ty + "))."); } String result = signatureResult.toString() + axiomsResult.toString() + conjecturesResult.toString(); return result.toString(); }

main

public static void main(java.lang.String[] args)

A test method.