[pagoda] Move project to Scala

This commit includes a few changes:
- The repository still uses Maven to manage dependency but it is now a
  Scala project.
- The code has been ported from OWLAPI 3.4.10 to 5.1.20
- A proof of concept program using both RSAComb and PAGOdA has been
  added.

3 files changed, 911 insertions, 0 deletions

diff --git a/src/main/java/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java b/src/main/java/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java
new file mode 100644
index 0000000..c3f7a2a
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java
@@ -0,0 +1,480 @@
+package uk.ac.ox.cs.pagoda.hermit;
+
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Map;
+import java.util.Set;
+
+import org.semanticweb.HermiT.Prefixes;
+import org.semanticweb.HermiT.model.AnnotatedEquality;
+import org.semanticweb.HermiT.model.AtLeastDataRange;
+import org.semanticweb.HermiT.model.Atom;
+import org.semanticweb.HermiT.model.AtomicConcept;
+import org.semanticweb.HermiT.model.AtomicDataRange;
+import org.semanticweb.HermiT.model.AtomicNegationDataRange;
+import org.semanticweb.HermiT.model.AtomicRole;
+import org.semanticweb.HermiT.model.Constant;
+import org.semanticweb.HermiT.model.ConstantEnumeration;
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.DLPredicate;
+import org.semanticweb.HermiT.model.Equality;
+import org.semanticweb.HermiT.model.Individual;
+import org.semanticweb.HermiT.model.Inequality;
+import org.semanticweb.HermiT.model.Term;
+import org.semanticweb.HermiT.model.Variable;
+
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+import uk.ac.ox.cs.pagoda.util.SparqlHelper;
+import uk.ac.ox.cs.pagoda.util.Utility;
+
+public class DLClauseHelper {
+
+        public static String getIRI4Nominal(DLPredicate predicate) {
+                return ((AtomicConcept) predicate).getIRI().replace("internal:nom#", "");
+        }
+
+        public static DLClause removeNominalConcept(DLClause clause) {
+                boolean hasNominals = false; 
+                Map<Variable, String> nom2iri = new HashMap<Variable, String>();
+                DLPredicate predicate;
+                Collection<Atom> remainingBodyAtoms = new LinkedList<Atom>();
+                for (Atom atom: clause.getBodyAtoms()) {
+                        predicate = atom.getDLPredicate();
+                        if (predicate instanceof AtomicConcept && predicate.toString().startsWith("<internal:nom#")) {
+                                nom2iri.put(atom.getArgumentVariable(0), getIRI4Nominal(predicate));
+                                hasNominals = true; 
+                        }
+                        else remainingBodyAtoms.add(atom);
+                }
+                
+                if (!hasNominals) return clause; 
+                
+                Atom[] newHeadAtoms = new Atom[clause.getHeadLength()];
+                int i = 0; 
+                for (Atom atom: clause.getHeadAtoms()) {
+                        newHeadAtoms[i++] = getNewAtom(atom, nom2iri); 
+                }
+                
+                Atom[] newBodyAtoms = new Atom[remainingBodyAtoms.size()]; 
+                i = 0; 
+                for (Atom atom: remainingBodyAtoms) {
+                        newBodyAtoms[i++] = getNewAtom(atom, nom2iri);  
+                }
+
+                return DLClause.create(newHeadAtoms, newBodyAtoms); 
+        }
+        
+        public static Atom getNewAtom(Atom atom, Map<Variable, String> nom2iri) {
+                String iri; 
+                DLPredicate predicate = atom.getDLPredicate();
+                if (predicate instanceof AtomicRole) { 
+                        boolean updated = false; 
+                        Term newArg0 = atom.getArgument(0), newArg1 = atom.getArgument(1);
+                        if (newArg0 instanceof Variable && ((iri = nom2iri.get((Variable) newArg0)) != null))  {
+                                newArg0 = Individual.create(iri); 
+                                updated = true; 
+                        }
+                        if (newArg1 instanceof Variable && ((iri = nom2iri.get((Variable) newArg1)) != null))  {
+                                newArg1 = Individual.create(iri); 
+                                updated = true; 
+                        }
+                        if (updated) {
+                                return Atom.create(atom.getDLPredicate(), newArg0, newArg1);
+                        }
+                }
+                else if (predicate instanceof Equality || predicate instanceof AnnotatedEquality) {
+//                      System.out.println("To be removed ... \n" + atom); 
+                        Term two[] = new Term[] { atom.getArgument(0), atom.getArgument(1) }; 
+                        Term t; 
+                        for (int i = 0; i < 2; ++i) {
+                                t = atom.getArgument(i);
+                                if (t != null && t instanceof Variable && (iri = nom2iri.get((Variable) t)) != null) {
+                                        two[i] = Individual.create(iri); 
+                                }
+                        }
+                        return Atom.create(Equality.INSTANCE, two);
+                }
+                
+                return atom; 
+        }
+        
+        /**
+         * This is a preprocess for StatOil:
+         *  
+         * if (AtomicNegationDataRange o (ConstantEnumerate (value))) (Z) 
+         * appears the head, then replace all Z in the clause by value. 
+         * 
+         * 
+         * @param clause
+         */
+        public static DLClause replaceWithDataValue(DLClause clause) {
+                Map<Variable, Constant> var2dataValue = new HashMap<Variable, Constant>();
+                
+                boolean update = false; 
+                LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
+                for (Atom cAtom: clause.getHeadAtoms()) {
+                        DLPredicate dlPredicate = cAtom.getDLPredicate();
+                        if (dlPredicate instanceof AtomicNegationDataRange) {
+                                AtomicDataRange atomicDataRange = ((AtomicNegationDataRange) dlPredicate).getNegatedDataRange(); 
+                                if (atomicDataRange instanceof ConstantEnumeration) {
+                                        ConstantEnumeration enumeration = (ConstantEnumeration) atomicDataRange;  
+                                        if (enumeration.getNumberOfConstants() == 1) {
+                                                Constant constant = enumeration.getConstant(0);
+                                                //TODO replace unsupported datatypes
+//                                              if (constant.getDatatypeURI().endsWith("boolean"))
+//                                                      constant = Constant.create(constant.getLexicalForm(), constant.getDatatypeURI().replace("boolean", "string"));  
+                                                var2dataValue.put(cAtom.getArgumentVariable(0), constant);
+                                        }
+                                }
+                        }
+                        else if (dlPredicate instanceof ConstantEnumeration) {
+                                ConstantEnumeration enu = (ConstantEnumeration) dlPredicate; 
+                                for (int i = 0; i < enu.getNumberOfConstants(); ++i) 
+                                        newHeadAtoms.add(Atom.create(Equality.INSTANCE, cAtom.getArgument(0), enu.getConstant(i)));
+                                update = true; 
+                        }
+                        else if (dlPredicate instanceof AtLeastDataRange &&     ((AtLeastDataRange) dlPredicate).getToDataRange() instanceof ConstantEnumeration) {
+                                AtLeastDataRange atLeast = (AtLeastDataRange) dlPredicate; 
+                                ConstantEnumeration enu = (ConstantEnumeration) atLeast.getToDataRange();
+                                for (int i = 0; i < enu.getNumberOfConstants(); ++i)
+                                        newHeadAtoms.add(Atom.create((AtomicRole) atLeast.getOnRole(), cAtom.getArgument(0), enu.getConstant(i)));
+                                update = true; 
+                        }
+                        else 
+                                newHeadAtoms.add(cAtom); 
+                }
+                
+                if (var2dataValue.isEmpty()) return update ? DLClause.create(newHeadAtoms.toArray(new Atom[0]), clause.getBodyAtoms()) : clause;
+                
+                Atom[] newBodyAtoms = new Atom[clause.getBodyLength()]; 
+                Term[] newArgs; 
+                int index = 0;
+                boolean atomUpdated; 
+                for (Atom bodyAtom: clause.getBodyAtoms()) {
+                        newBodyAtoms[index] = bodyAtom;
+                        atomUpdated = false; 
+                        newArgs = new Term[bodyAtom.getArity()]; 
+                        for (int i = 0; i < newArgs.length; ++i) {
+                                newArgs[i] = bodyAtom.getArgument(i); 
+                                if (newArgs[i] instanceof Variable && var2dataValue.containsKey(newArgs[i])) { 
+                                        newArgs[i] = var2dataValue.get(newArgs[i]);
+                                        atomUpdated = true; 
+                                }
+                        }
+                        if (atomUpdated)
+                                newBodyAtoms[index] = Atom.create(bodyAtom.getDLPredicate(), newArgs);
+                        ++index; 
+                }
+
+                return DLClause.create(newHeadAtoms.toArray(new Atom[0]), newBodyAtoms); 
+        }
+        
+        public static DLClause simplified(DLClause clause) {
+                TermGraph termGraph = new TermGraph(clause); 
+                return termGraph.simplify(); 
+        }
+
+        public static DLClause contructor_differentFrom(Individual u,   Individual v) {
+                Atom equalityAtom = Atom.create(AtomicRole.create(Namespace.EQUALITY), u, v);
+                return DLClause.create(new Atom[0], new Atom[] {equalityAtom});  
+        }
+        
+        public static String toString(Collection<DLClause> clauses) {
+                StringBuilder buf = new StringBuilder();
+                for (DLClause cls: clauses) {
+                        buf.append(RuleHelper.getText(cls));
+                        buf.append(Utility.LINE_SEPARATOR); 
+                }
+                return buf.toString(); 
+        }
+
+        public static DLClause getInstance(DLClause queryClause, Map<Variable, Term> assignment) {
+                Atom[] newBodyAtoms = new Atom[queryClause.getBodyLength()];
+                int index = 0; 
+                for (Atom atom: queryClause.getBodyAtoms()) {
+                        newBodyAtoms[index++] = getInstance(atom, assignment); 
+                }
+                return DLClause.create(queryClause.getHeadAtoms(), newBodyAtoms);
+        }
+        
+        public static Atom getInstance(Atom atom, Map<Variable, Term> assignment) {
+                Term[] args = getArguments(atom);
+                for (int i = 0; i < args.length; ++i)
+                        args[i] = getInstance(args[i], assignment); 
+                return Atom.create(atom.getDLPredicate(), args);
+        }
+        
+        private static Term getInstance(Term t, Map<Variable, Term> assignment) {
+                if (t instanceof Variable && assignment.containsKey((Variable) t)) 
+                        return assignment.get(t);
+                return t;
+        }
+
+        public static Term[] getArguments(Atom atom) {
+                int len = atom.getArity(); 
+                if (len >= 2) len = 2; 
+                Term[] args = new Term[len];
+                for (int i = 0; i < len; ++i)
+                        args[i] = atom.getArgument(i);
+                return args;
+        }
+        
+        public static DLClause getQuery(String queryText, Collection<String> answerVariables) {
+                Collection<Atom> bodyAtoms = new LinkedList<Atom>();
+                SparqlHelper.parse(queryText.replace("_:", "?"), answerVariables, bodyAtoms);
+                return DLClause.create(new Atom[0], bodyAtoms.toArray(new Atom[0]));
+        }
+        
+        public static DLClause getQuery_old(String queryText, Collection<String> answerVariables) {
+                String key, value;
+                Prefixes prefixes = new Prefixes(); 
+                if (answerVariables != null) 
+                        answerVariables.clear();
+                String[] temp;
+                Term subject, object;
+                LinkedList<Atom> bodyAtoms = new LinkedList<Atom>(); 
+
+                for (String line: queryText.split("\n")) {
+                        line = line.trim(); 
+                        if (line.startsWith("PREFIX")) {
+                                key = line.substring(7, line.indexOf(':') + 1);
+                                value = line.substring(line.indexOf('<') + 1, line.length() - 1);
+                                prefixes.declarePrefix(key, value);
+                        } 
+                        else if (line.startsWith("SELECT")) {
+                                if (answerVariables == null)
+                                        continue;
+                                temp = line.split(" ");
+                                for (int i = 1; i < temp.length; ++i)
+                                        answerVariables.add(temp[i].substring(1));
+                        } 
+                        else if (line.startsWith("WHERE"))
+                                ;
+                        else if (line.startsWith("}"))
+                                ;
+                        else {
+                                temp = line.split(" ");
+                                subject = getTerm(getAbsoluteIRI(temp[0], prefixes));
+                                temp[1] = getAbsoluteIRI(temp[1], prefixes);
+                                temp[2] = getAbsoluteIRI(temp[2], prefixes); 
+                                if (temp[1].equals(Namespace.RDF_TYPE)) {
+                                        temp[2] = getAbsoluteIRI(temp[2], prefixes); 
+                                        bodyAtoms.add(Atom.create(AtomicConcept.create(temp[2]), subject));
+                                } else {
+                                        object = getTerm(temp[2]);
+                                        Term[] args = {subject, object};
+                                        bodyAtoms.add(Atom.create(AtomicRole.create(temp[1]), args));
+                                }
+                        }
+                }
+
+                return DLClause.create(new Atom[0], bodyAtoms.toArray(new Atom[0]));
+        }
+
+        private static String getAbsoluteIRI(String iri, Prefixes prefixes) {
+                if (prefixes.canBeExpanded(iri)) 
+                        return prefixes.expandAbbreviatedIRI(iri);
+                if (iri.startsWith("<"))
+                        return OWLHelper.removeAngles(iri);
+                return iri; 
+        }
+
+        private static Term getTerm(String iri) {
+                if (iri.startsWith("?"))
+                        return Variable.create(iri.substring(1));
+                else if (iri.contains("http")) 
+                        return Individual.create(iri); 
+                else 
+                        return getConstant(iri); 
+        }
+
+        private static Constant getConstant(String iri) {
+                String lexicalForm, datatypeIRI; 
+                int index = iri.indexOf("^^"); 
+                if (index == -1) { 
+                        lexicalForm = iri;
+                        int atPos = iri.indexOf("@"); 
+                        datatypeIRI = atPos == -1 ? Namespace.XSD_STRING : Namespace.RDF_PLAIN_LITERAL;
+                }
+                else { 
+                        if (iri.charAt(index + 2) == '<')
+                                datatypeIRI = iri.substring(index + 3, iri.length() - 1);
+                        else 
+                                datatypeIRI = iri.substring(index + 2);
+                        lexicalForm = iri.substring(1, index - 1); 
+                }
+                return Constant.create(lexicalForm, datatypeIRI); 
+        }
+
+        public static boolean isFunctionalDataPropertyAxioms(DLClause dlClause) {
+                 if (dlClause.getBodyLength()==2 && dlClause.getHeadLength()==1) {
+                    DLPredicate atomicRole=dlClause.getBodyAtom(0).getDLPredicate();
+                    if (atomicRole instanceof AtomicRole) {
+                        if (dlClause.getBodyAtom(1).getDLPredicate().equals(atomicRole) && 
+                                        (dlClause.getHeadAtom(0).getDLPredicate() instanceof Equality ||
+                                                        dlClause.getHeadAtom(0).getDLPredicate() instanceof AnnotatedEquality)) {
+                            Variable x=dlClause.getBodyAtom(0).getArgumentVariable(0);
+                            if (x!=null && x.equals(dlClause.getBodyAtom(1).getArgument(0))) {
+                                Variable y1=dlClause.getBodyAtom(0).getArgumentVariable(1);
+                                Variable y2=dlClause.getBodyAtom(1).getArgumentVariable(1);
+                                Variable headY1=dlClause.getHeadAtom(0).getArgumentVariable(0);
+                                Variable headY2=dlClause.getHeadAtom(0).getArgumentVariable(1);
+                                if (y1!=null && y2!=null && !y1.equals(y2) && headY1!=null && headY2!=null && ((y1.equals(headY1) && y2.equals(headY2)) || (y1.equals(headY2) && y2.equals(headY1))))
+                                    return true;
+                            }
+                        }
+                    }
+                }
+                return false;
+        }
+        
+        /**
+         * 
+         * @param dlClause
+         * @return 000 -> 111 R \circ S \sqsubseteq T if R, S, T is inverse. -1 if it is not a role composition axiom.
+         */
+        public static int isRoleCompositionAxioms(DLClause dlClause) {
+                 if (dlClause.getBodyLength()==2 && dlClause.getHeadLength()==1) {
+                         Atom body1 = dlClause.getBodyAtom(0), body2 = dlClause.getBodyAtom(1);
+                         Atom head = dlClause.getHeadAtom(0); 
+                         if (!(head.getDLPredicate() instanceof AtomicRole)) return -1; 
+                         if (!(body1.getDLPredicate() instanceof AtomicRole)) return -1;
+                         if (!(body2.getDLPredicate() instanceof AtomicRole)) return -1;
+                         if (!(head.getArgument(0) instanceof Variable)) return -1;
+                         if (!(head.getArgument(1) instanceof Variable)) return -1;
+                         if (!(body1.getArgument(0) instanceof Variable)) return -1;
+                         if (!(body1.getArgument(1) instanceof Variable)) return -1;
+                         if (!(body2.getArgument(0) instanceof Variable)) return -1;
+                         if (!(body2.getArgument(1) instanceof Variable)) return -1;
+                         Variable rx, ry, sx, sy, tx, ty;
+                         tx = head.getArgumentVariable(0); ty = head.getArgumentVariable(1); 
+                         rx = body1.getArgumentVariable(0); ry = body1.getArgumentVariable(1); 
+                         sx = body2.getArgumentVariable(0); sy = body2.getArgumentVariable(1);
+                         
+                         if (rx.equals(tx))
+                                 if (ry.equals(sx))
+                                         if (sy.equals(ty)) return 0; 
+                                         else return -1; 
+                                 else if (ry.equals(sy))
+                                         if (sx.equals(ty)) return 2;
+                                         else return -1; 
+                                 else 
+                                         return -1; 
+                         else if (rx.equals(ty))
+                                 if (ry.equals(sx))
+                                         if (sy.equals(tx)) return 1; 
+                                         else return -1; 
+                                 else if (ry.equals(sy))
+                                         if (sx.equals(tx)) return 3; 
+                                         else return -1; 
+                                 else
+                                         return -1; 
+                         else if (ry.equals(tx)) 
+                                 if (rx.equals(sx))
+                                         if (sy.equals(ty)) return 4; 
+                                         else return -1; 
+                                 else if (rx.equals(sy))
+                                         if (sx.equals(ty)) return 6; 
+                                         else return -1; 
+                                 else 
+                                         return -1; 
+                         else if (ry.equals(ty))
+                                 if (rx.equals(sx))
+                                         if (sy.equals(tx)) return 5; 
+                                         else return -1; 
+                                 else if (rx.equals(sy))
+                                         if (sx.equals(tx)) return 7; 
+                                         else return -1; 
+                                 else return -1; 
+                         else 
+                                 return -1; 
+                 }
+                 return -1;
+        }
+
+        public static boolean isGround(Atom tHeadAtom) {
+                for (int i = 0; i < tHeadAtom.getArity(); ++i)
+                        if (tHeadAtom.getArgument(i) instanceof Variable)
+                                return false; 
+                return true;
+        }
+        /**
+         * true if a \subseteq b
+         * @param a
+         * @param b
+         * @return
+         */
+        private static boolean hasSubsetAtoms(Atom[] a, Atom[] b) {
+                Set<String> atoms = new HashSet<String>();
+                for (int i = 0; i < b.length; ++i)
+                        atoms.add(b[i].toString()); 
+                
+                for (int i = 0; i < a.length; ++i)
+                        if (!atoms.remove(a[i].toString()))
+                                return false; 
+                
+                return true;
+        }
+
+        public static boolean hasSubsetBodyAtoms(DLClause c1, DLClause c2) {
+                return hasSubsetAtoms(c1.getBodyAtoms(), c2.getBodyAtoms()); 
+        }
+
+        public static DLClause replaceOtherBottom(DLClause dlClause) {
+                Atom[] newHeadAtoms = dlClause.getHeadAtoms(), newBodyAtoms = dlClause.getBodyAtoms();
+                if (containsOtherBottom(newHeadAtoms))
+                        newHeadAtoms = replaceOtherBottom(newHeadAtoms); 
+                if (containsOtherBottom(newBodyAtoms))
+                        newBodyAtoms = replaceOtherBottom(newBodyAtoms); 
+
+                if (newHeadAtoms == dlClause.getHeadAtoms() && newBodyAtoms == dlClause.getBodyAtoms())
+                        return dlClause;
+                
+                return DLClause.create(newHeadAtoms, newBodyAtoms); 
+        }
+        
+        private static Atom[] replaceOtherBottom(Atom[] atoms) {
+                Atom[] newAtoms = new Atom[atoms.length];
+                int index = 0; 
+                for (Atom atom: atoms) 
+                        if (isOtherBottom(atom.getDLPredicate()))
+                                newAtoms[index++] = Atom.create(AtomicConcept.NOTHING, atom.getArgument(0)); 
+                        else 
+                                newAtoms[index++] = atom;
+                return newAtoms; 
+        }
+
+        private static boolean isOtherBottom(DLPredicate p) {
+                if (!(p instanceof AtomicConcept)) return false; 
+                
+                String name = p.toString();
+                int index; 
+                char ch; 
+                if ((index = name.indexOf("owl:Nothing")) != -1) {
+                        index += 11; 
+                        if (name.length() <= index) return true;  
+                        if ((ch = name.charAt(index)) == '_') return true; 
+                        if (ch >= '0' && ch <= '9') return true; 
+                }
+                return false; 
+        }
+        
+        private static boolean containsOtherBottom(Atom[] atoms) {
+                for (Atom atom: atoms) 
+                        if (isOtherBottom(atom.getDLPredicate()))
+                                return true; 
+                return false; 
+        }
+
+        public static boolean isTautologyAboutDifferentFrom(DLClause clause) {
+                if (clause.getHeadLength() > 1 || clause.getBodyLength() != 1) return false;
+                if (clause.getHeadLength() == 1 && !clause.getHeadAtom(0).getDLPredicate().toString().contains(AtomicConcept.NOTHING.toString()))
+                        return false;
+                Atom bodyAtom = clause.getBodyAtom(0); 
+                return (bodyAtom.getDLPredicate() instanceof Inequality) && bodyAtom.getArgument(0).equals(bodyAtom.getArgument(1)); 
+        }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java b/src/main/java/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
new file mode 100644
index 0000000..43c5849
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/hermit/RuleHelper.java
@@ -0,0 +1,173 @@
+package uk.ac.ox.cs.pagoda.hermit;
+
+import org.semanticweb.HermiT.model.*;
+import uk.ac.ox.cs.pagoda.MyPrefixes;
+import uk.ac.ox.cs.pagoda.owl.OWLHelper;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+
+import java.security.InvalidParameterException;
+import java.util.ArrayList;
+
+public class RuleHelper {
+    private static final String OR = "|";
+    private static final String IF = ":-";
+    private static final String AND = ",";
+
+//      public static String abbreviateIRI(String text) {
+//              String prefixName, prefixIRI; 
+//              int start = -1, ends = -1;
+//              while (true) {
+//                      start = text.indexOf('<', ends + 1);
+//                      if (start == -1) return text;
+//                      ends = text.indexOf('>', start + 1);
+//                      if (ends == -1) return text;
+//                      String sub = text.substring(start, ends + 1), newSub = text.substring(start + 1, ends);
+//                      
+//                      int index = splitPoint(newSub); 
+//                      if (index >= 0) {
+//                              prefixIRI = newSub.substring(0, index + 1);
+//                              if ((prefixName = MyPrefixes.PAGOdAPrefixes.getPrefixName(prefixIRI)) == null) {
+//                                      prefixName = getNewPrefixName();
+//                                      MyPrefixes.PAGOdAPrefixes.declarePrefix(prefixName, prefixIRI);
+//                              }
+//                              newSub = newSub.replace(prefixIRI, prefixName); 
+//                              text = text.replaceAll(sub, newSub);
+//                              ends -= sub.length() - newSub.length();
+//                      }
+//              }
+//      }
+        
+        public static String getText(DLClause clause) {
+                StringBuffer buf = new StringBuffer();
+                String atomText; 
+                
+                boolean lastSpace = true;
+                for (Atom headAtom: clause.getHeadAtoms()) {
+                        if ((atomText = getText(headAtom)) == null) continue; 
+                        if (!lastSpace) buf.append(" ").append(OR).append(" ");
+                        buf.append(atomText);
+                        lastSpace = false;
+                }
+        buf.append(" ").append(IF).append(" ");
+                lastSpace = true;
+                for (Atom bodyAtom: clause.getBodyAtoms()) {
+//              for (String str: strs[1].split(", ")) {
+                        if ((atomText = getText(bodyAtom)) == null) continue; 
+                        if (!lastSpace) buf.append(AND).append(" ");
+                        buf.append(atomText);
+                        lastSpace = false;
+                }
+                buf.append('.');
+                return buf.toString();
+        }
+
+        
+        private static String getText(Atom atom) {
+                if (atom.getDLPredicate() instanceof NodeIDsAscendingOrEqual ||
+                                atom.getDLPredicate() instanceof NodeIDLessEqualThan) 
+                        return null;
+                
+                StringBuilder builder = new StringBuilder(); 
+                if (atom.getArity() == 1) {
+                        builder.append(getText(atom.getDLPredicate())); 
+                        builder.append("("); 
+                        builder.append(getText(atom.getArgument(0)));
+                        builder.append(")"); 
+                }
+                else {
+                        DLPredicate p = atom.getDLPredicate();
+                        if (p instanceof Equality || p instanceof AnnotatedEquality) builder.append(Namespace.EQUALITY_ABBR); 
+                        else if (p instanceof Inequality) builder.append(Namespace.INEQUALITY_ABBR); 
+                        else builder.append(getText(p));
+                        builder.append("("); 
+                        builder.append(getText(atom.getArgument(0))); 
+                        builder.append(",");
+                        builder.append(getText(atom.getArgument(1))); 
+                        builder.append(")"); 
+                }
+                return builder.toString(); 
+        }
+
+        public static String getText(DLPredicate p) {
+                if (p instanceof Equality || p instanceof AnnotatedEquality) return Namespace.EQUALITY_ABBR; 
+                if (p instanceof Inequality) return Namespace.INEQUALITY_ABBR;
+                if (p instanceof AtomicRole && ((AtomicRole) p).getIRI().startsWith("?"))
+                        return ((AtomicRole) p).getIRI(); 
+                return MyPrefixes.PAGOdAPrefixes.abbreviateIRI(p.toString());
+        }
+
+        public static String getText(Term t) {
+                if (t instanceof Variable)
+                        return "?" + ((Variable) t).getName(); 
+                return MyPrefixes.PAGOdAPrefixes.abbreviateIRI(t.toString());
+        }
+
+        public static Term parseTerm(String s) {
+                s = s.trim();
+                if(s.startsWith("?")) return Variable.create(s.substring(1));
+                return Individual.create(MyPrefixes.PAGOdAPrefixes.expandIRI(s));
+        }
+
+    public static Atom parseAtom(String s) {
+        s = s.trim();
+
+        String[] split = s.split("\\(");
+        String predicateIri = OWLHelper.removeAngles(MyPrefixes.PAGOdAPrefixes.expandText(split[0]));
+        String[] predicateArgs = split[1].substring(0, split[1].length() - 1).split(",");
+        int numOfargs = predicateArgs.length;
+        Term terms[] = new Term[predicateArgs.length];
+        for (int i = 0; i < terms.length; i++)
+            terms[i] = parseTerm(predicateArgs[i]);
+        if(numOfargs == 1) {
+            AtomicConcept atomicConcept = AtomicConcept.create(predicateIri);
+            return Atom.create(atomicConcept, terms);
+        }
+        else if(numOfargs == 2) {
+            AtomicRole atomicRole = AtomicRole.create(predicateIri);
+            return Atom.create(atomicRole, terms);
+        }
+        else
+            throw new InvalidParameterException();
+        // TODO? add equality (owl:sameAs)?
+    }
+
+    public static DLClause parseClause(String s) {
+        s = s.trim();
+        if(s.endsWith(".")) s = s.substring(0, s.length()-1).trim();
+
+        String[] headAndBody = s.split(IF);
+        String[] headAtomsStr = splitAtoms(headAndBody[0], OR);
+        String[] bodyAtomsStr = splitAtoms(headAndBody[1], AND);
+
+        Atom[] headAtoms = new Atom[headAtomsStr.length];
+        Atom[] bodyAtoms = new Atom[bodyAtomsStr.length];
+        for (int i = 0; i < headAtoms.length; i++)
+            headAtoms[i] = parseAtom(headAtomsStr[i]);
+        for (int i = 0; i < bodyAtoms.length; i++)
+            bodyAtoms[i] = parseAtom(bodyAtomsStr[i]);
+
+        return DLClause.create(headAtoms, bodyAtoms);
+    }
+
+    private static String[] splitAtoms(String s, String operator) {
+        char op = operator.charAt(0);
+        ArrayList<String> result = new ArrayList<>();
+
+        int b = 0;
+        boolean betweenParenthesis = false;
+        for (int i = 0; i < s.length(); i++) {
+            if(s.charAt(i) == '(')
+                betweenParenthesis = true;
+            else if(s.charAt(i) == ')')
+                betweenParenthesis = false;
+            else if(s.charAt(i) == op && !betweenParenthesis) {
+                result.add(s.substring(b, i));
+                b = i + 1;
+            }
+        }
+        if(b < s.length()) result.add(s.substring(b));
+
+        return result.toArray(new String[0]);
+    }
+
+}
diff --git a/src/main/java/uk/ac/ox/cs/pagoda/hermit/TermGraph.java b/src/main/java/uk/ac/ox/cs/pagoda/hermit/TermGraph.java
new file mode 100644
index 0000000..0041cca
--- /dev/null
+++ b/src/main/java/uk/ac/ox/cs/pagoda/hermit/TermGraph.java
@@ -0,0 +1,258 @@
+package uk.ac.ox.cs.pagoda.hermit;
+
+import java.util.Collection;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Map;
+import java.util.PriorityQueue;
+import java.util.Set;
+
+import org.semanticweb.HermiT.model.AnnotatedEquality;
+import org.semanticweb.HermiT.model.Atom;
+import org.semanticweb.HermiT.model.AtomicConcept;
+import org.semanticweb.HermiT.model.AtomicRole;
+import org.semanticweb.HermiT.model.Constant;
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.DLPredicate;
+import org.semanticweb.HermiT.model.DatatypeRestriction;
+import org.semanticweb.HermiT.model.Equality;
+import org.semanticweb.HermiT.model.Individual;
+import org.semanticweb.HermiT.model.NodeIDLessEqualThan;
+import org.semanticweb.HermiT.model.NodeIDsAscendingOrEqual;
+import org.semanticweb.HermiT.model.Term;
+import org.semanticweb.HermiT.model.Variable;
+
+import uk.ac.ox.cs.pagoda.util.Namespace;
+import uk.ac.ox.cs.pagoda.util.Utility;
+
+public class TermGraph {
+        
+        Map<Term, Collection<Edge>> graph = new HashMap<Term, Collection<Edge>>(); 
+        Map<Term, Collection<AtomicConcept>> term2concepts = new HashMap<Term, Collection<AtomicConcept>>();
+        Set<Term> choosen = new HashSet<Term>(), allTerms = new HashSet<Term>(); 
+        DLClause clause;
+        Set<Atom> newBodyAtoms = new HashSet<Atom>(); 
+
+        public TermGraph(DLClause clause) {
+                this.clause = clause; 
+                for (Atom atom: clause.getHeadAtoms())
+                        for (int i = 0; i < atom.getArity(); ++i)
+                                allTerms.add(atom.getArgument(i)); 
+                for (Atom atom: clause.getBodyAtoms())
+                        for (int i = 0; i < atom.getArity(); ++i)
+                                allTerms.add(atom.getArgument(i)); 
+        }
+        
+        public DLClause simplify() {
+                constructGraph(); 
+                chooseTerms(); 
+                
+                PriorityQueue<Term> queue = new PriorityQueue<Term>(allTerms.size(), new Comparator<Term>() {
+
+                        @Override
+                        public int compare(Term o1, Term o2) {
+                                int diff = 0; 
+                                @SuppressWarnings("rawtypes")
+                                Collection set1 = term2concepts.get(o1), set2 = term2concepts.get(o2);
+                                int num1 = size(set1), num2 = size(set2); 
+                                
+                                if ((diff = num2 - num1) != 0) 
+                                        return diff;
+                                
+                                set1 = graph.get(o1); set2 = graph.get(o2); 
+                                num1 = size(set1); num2 = size(set2); 
+                                
+                                return num2 - num1; 
+                        }
+                        
+                        private int size(@SuppressWarnings("rawtypes") Collection c) {
+                                return c == null ? 0 : c.size();
+                        }
+                        
+                });
+                
+                for (Term term: allTerms)
+                        queue.add(term);
+                
+                while (!queue.isEmpty()) {
+                        Term term = queue.remove();
+                        if (!choosen.contains(term) && isRepresentative(term)) 
+                                choosen.add(term);
+                }
+
+                boolean flag; 
+                for (Iterator<Atom> iter = newBodyAtoms.iterator(); iter.hasNext(); ) {
+                        flag = true; 
+                        Atom atom = iter.next(); 
+                        for (int i = 0; i < atom.getArity(); ++i) {
+                                if (!choosen.contains(atom.getArgument(i))) {
+                                        flag = false; 
+                                        break; 
+                                }
+                        }
+                        if (!flag) iter.remove(); 
+                }
+                
+                return DLClause.create(clause.getHeadAtoms(), newBodyAtoms.toArray(new Atom[0])); 
+        }
+        
+        private boolean isRepresentative(Term term) {
+                boolean flag = true; 
+                for (Term otherTerm: choosen) 
+                        if (!term.equals(otherTerm) && isSubsumedBy(term, otherTerm)) {
+                                flag = false; 
+                        }
+                return flag;
+        }
+        
+        private boolean isSubsumedBy(Term t1, Term t2) {
+                Collection<AtomicConcept> set1 = term2concepts.get(t1);
+                Collection<AtomicConcept> set2 = term2concepts.get(t2);
+                
+                if (set1 != null)
+                        if (set2 == null)
+                                return false;
+                        else if (!set2.containsAll(set1))
+                                return false; 
+                
+                Collection<Edge> edgeSet1 = graph.get(t1);  
+                Collection<Edge> edgeSet2 = graph.get(t2);
+                if (edgeSet1 != null)
+                        if (edgeSet2 == null)
+                                return false; 
+                        else {
+                                if (!edgeSet2.containsAll(edgeSet1))
+                                        return false;
+//                              else {
+//                                      Collection<Edge> restEdge1 = new HashSet<Edge>(); 
+//                                      for (Edge edge: edgeSet1)
+//                                              if (edge.term == t2); 
+//                                              else restEdge1.add(edge);
+//                                      
+//                                      Collection<Edge> restEdge2 = new HashSet<Edge>(); 
+//                                      for (Edge edge: edgeSet2)
+//                                              if (edge.term == t1); 
+//                                              else restEdge2.add(edge);
+//                                      
+//                                      return restEdge2.containsAll(edgeSet1);
+//                              }
+                        }
+                
+                return true; 
+        }
+
+        private void chooseTerms() {
+                Set<Variable> headVariables = new HashSet<Variable>(); 
+                for (Atom atom: clause.getHeadAtoms()) {
+                        atom.getVariables(headVariables);
+                }
+                choosen.addAll(headVariables); 
+                
+                for (Term term: allTerms) 
+                        if (term instanceof Constant || term instanceof Individual)
+                                choosen.add(term);
+
+                if (choosen.isEmpty()) choosen.add(Variable.create("X")); 
+//              propagate();
+        }
+
+//      private void propagate() {
+//              LinkedList<Term> queue = new LinkedList<Term>(choosen);
+//              Term term; 
+//              while (!queue.isEmpty()) {
+//                      term = queue.pop(); 
+//                      if (graph.containsKey(term))
+//                              for (Edge edge: graph.get(term)) 
+//                                      if (!choosen.contains(edge.term)) {
+//                                              choosen.add(edge.term); 
+//                                              queue.add(term); 
+//                                      }
+//              }
+//      }
+
+        private void constructGraph() {
+                DLPredicate p; 
+                for (Atom bodyAtom: clause.getBodyAtoms()) {
+                        p = bodyAtom.getDLPredicate(); 
+                        if (p instanceof AtomicConcept) {
+                                newBodyAtoms.add(bodyAtom); 
+                                addConcept(bodyAtom.getArgument(0), (AtomicConcept) p);
+                        }
+                        else if (p instanceof AtomicRole) {
+                                newBodyAtoms.add(bodyAtom); 
+                                addEdges(bodyAtom.getArgument(0), bodyAtom.getArgument(1), (AtomicRole) p);
+                        }
+                        else if (p instanceof DatatypeRestriction) 
+                                newBodyAtoms.add(bodyAtom); 
+                        else if (p instanceof NodeIDLessEqualThan || p instanceof NodeIDsAscendingOrEqual);  
+                        else if (p instanceof Equality || p instanceof AnnotatedEquality) {
+                                newBodyAtoms.add(bodyAtom); 
+                                addEdges(bodyAtom.getArgument(0), bodyAtom.getArgument(1), AtomicRole.create(Namespace.EQUALITY)); 
+                        } else {
+                                Utility.logError("Unknown DLPredicate in TermGraph: " + p);
+                        }
+                }
+        }
+        
+        private void addEdges(Term t1, Term t2, AtomicRole p) {
+                addEdge(t1, new Edge(p, t2, false));
+                addEdge(t2, new Edge(p, t1, true)); 
+        }
+
+        private void addEdge(Term t, Edge edge) {
+                Collection<Edge> edges; 
+                if ((edges = graph.get(t)) == null) {
+                        graph.put(t, edges = new HashSet<Edge>()); 
+                }
+                edges.add(edge);                
+        }
+
+        private void addConcept(Term t, AtomicConcept p) {
+                Collection<AtomicConcept> concepts; 
+                if ((concepts = term2concepts.get(t)) == null) {
+                        term2concepts.put(t, concepts = new HashSet<AtomicConcept>()); 
+                }
+                concepts.add(p);                
+        }
+
+        public boolean mark(Term t) {
+                return choosen.add(t);  
+        }
+        
+}
+
+class Edge {
+        boolean isInverse; 
+        AtomicRole role; 
+        Term term; 
+        
+        public Edge(AtomicRole role, Term term, boolean isInverse) {
+                this.role = role; 
+                this.term = term; 
+                this.isInverse = isInverse; 
+        }
+        
+        @Override
+        public int hashCode() {
+                return role.hashCode() * 1997 + term.hashCode() * 2 + (isInverse ? 1 : 0); 
+        }
+        
+        @Override
+        public boolean equals(Object obj) {
+                if (!(obj instanceof Edge)) return false; 
+                Edge other = (Edge) obj; 
+                return isInverse == other.isInverse && role.equals(other.role) && term.equals(other.term);  
+        }
+        
+        @Override
+        public String toString() {
+                if (isInverse)
+                        return "inv_" + role.toString() + "_" + term.toString();
+                return role.toString() + "_" + term.toString();
+        }
+        
+}
+
+