[DL-Learner SVN] SF.net SVN: dl-learner:[2857] trunk/components-core/src

[<ji...@us...>]

Revision: 2857
          http://dl-learner.svn.sourceforge.net/dl-learner/?rev=2857&view=rev
Author:   jialva
Date:     2011-06-08 18:10:11 +0000 (Wed, 08 Jun 2011)

Log Message:
-----------
New update of fuzzyDL-Learner

Modified Paths:
--------------
    trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java
    trunk/components-core/src/main/java/org/dllearner/core/ReasonerComponent.java
    trunk/components-core/src/main/java/org/dllearner/core/fuzzydll/FuzzyIndividualReasoner.java
    trunk/components-core/src/main/java/org/dllearner/learningproblems/fuzzydll/FuzzyPosNegLPStandard.java
    trunk/components-core/src/main/java/org/dllearner/reasoning/fuzzydll/FuzzyOWLAPIReasoner.java
    trunk/components-core/src/test/java/org/dllearner/test/FuzzyDLLTest_Trains.java
    trunk/components-core/src/test/java/org/dllearner/test/FuzzyDLLTest_noFuzzyTrains.java

Added Paths:
-----------
    trunk/components-core/src/main/java/org/dllearner/refinementoperators/fuzzydll/
    trunk/components-core/src/main/java/org/dllearner/refinementoperators/fuzzydll/FuzzyRhoDRDown.java
    trunk/components-core/src/test/java/org/dllearner/test/FuzzyDLLTest_Trains_noFuzzyIndividuals.java

Modified: trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java	2011-06-08 12:11:40 UTC (rev 2856)
+++ trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java	2011-06-08 18:10:11 UTC (rev 2857)
@@ -19,7 +19,11 @@
  */
 package org.dllearner.algorithms.fuzzydll;
 
+import java.io.BufferedWriter;
 import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
+import java.io.PrintWriter;
 import java.text.DecimalFormat;
 import java.util.Collection;
 import java.util.Iterator;
@@ -59,6 +63,7 @@
 import org.dllearner.refinementoperators.OperatorInverter;
 import org.dllearner.refinementoperators.RefinementOperator;
 import org.dllearner.refinementoperators.RhoDRDown;
+import org.dllearner.refinementoperators.fuzzydll.FuzzyRhoDRDown;
 import org.dllearner.utilities.Files;
 import org.dllearner.utilities.Helper;
 import org.dllearner.utilities.owl.ConceptComparator;
@@ -144,6 +149,10 @@
 	private int minHorizExp = 0;
 	private int maxHorizExp = 0;
 	
+	// TODO remove this variable, just for testing purposes
+	private int counter = 0;
+	private PrintWriter out;
+	
 	@Override
 	public FuzzyCELOEConfigurator getConfigurator() {
 		return configurator;
@@ -196,6 +205,17 @@
 	
 	@Override
 	public void init() throws ComponentInitException {
+		
+		// TODO remove, just for testing purposes
+		FileWriter fstream;
+		try {			
+			fstream = new FileWriter("../examples/fuzzydll/testOut_TriRecEq.log");
+			out = new PrintWriter(fstream);
+		} catch (IOException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+		
 		// copy class hierarchy and modify it such that each class is only
 		// reachable via a single path
 		ClassHierarchy classHierarchy = reasoner.getClassHierarchy().clone();
@@ -210,7 +230,7 @@
 		singleSuggestionMode = configurator.getSingleSuggestionMode();
 		
 		// create refinement operator
-		operator = new RhoDRDown(reasoner, classHierarchy, startClass, configurator);
+		operator = new FuzzyRhoDRDown(reasoner, classHierarchy, startClass, configurator);
 		baseURI = reasoner.getBaseURI();
 		prefixes = reasoner.getPrefixes();		
 		if(configurator.getWriteSearchTree()) {
@@ -315,7 +335,6 @@
 		} else if (learningProblem instanceof FuzzyPosNegLP) {
 			examples = Helper.union(((FuzzyPosNegLP)learningProblem).getPositiveExamples(),((FuzzyPosNegLP)learningProblem).getNegativeExamples());
 		}
-		
 	}
 
 	@Override
@@ -375,12 +394,15 @@
 			Monitor mon = MonitorFactory.start("refineNode");
 			TreeSet<Description> refinements = refineNode(nextNode);
 			mon.stop();
-				
-//			System.out.println("next node: " + nextNode);
-//			for(Description refinement : refinements) {
-//				System.out.println("refinement: " + refinement);
-//			}
 			
+			// TODO just for testing purposes
+			counter++;
+			System.out.println(counter + " next node: " + nextNode);
+			for(Description refinement : refinements) {
+				System.out.println("refinement: " + refinement);
+			}
+			System.out.println();
+			
 			while(refinements.size() != 0) {
 				// pick element from set
 				Description refinement = refinements.pollFirst();
@@ -483,20 +505,18 @@
 	// add node to search tree if it is not too weak
 	// returns true if node was added and false otherwise
 	private boolean addNode(Description description, FuzzyOENode parentNode) {
-		
-//		System.out.println(description);
-		
+		// counter++;
+		// System.out.println(counter + " " + description);
+
 		// redundancy check (return if redundant)
 		boolean nonRedundant = descriptions.add(description);
 		if(!nonRedundant) {
 			return false;
 		}
-		
 		// check whether the description is allowed
 		if(!isDescriptionAllowed(description, parentNode)) {
 			return false;
-		}
-		
+		}	
 //		System.out.println("Test " + new Date());
 		// quality of description (return if too weak)
 		double accuracy = learningProblem.getAccuracyOrTooWeak(description, noise);
@@ -544,6 +564,18 @@
 		// necessary since rewriting is expensive
 		boolean isCandidate = !bestEvaluatedDescriptions.isFull();
 		if(!isCandidate) {
+			
+			// TODO remove, just testing purposes
+//			Iterator i = bestEvaluatedDescriptions.getSet().iterator();
+//			int j = 0;
+//			out.println(counter + " " + description);
+//			while (i.hasNext()) {
+//				j++;
+//				// System.err.println(j + " -> " + i.next());
+//				out.println(j + " -> " + i.next());
+//			}
+//			out.println();
+			
 			EvaluatedDescription worst = bestEvaluatedDescriptions.getWorst();
 			double accThreshold = worst.getAccuracy();
 			isCandidate = 

Modified: trunk/components-core/src/main/java/org/dllearner/core/ReasonerComponent.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/core/ReasonerComponent.java	2011-06-08 12:11:40 UTC (rev 2856)
+++ trunk/components-core/src/main/java/org/dllearner/core/ReasonerComponent.java	2011-06-08 18:10:11 UTC (rev 2857)
@@ -358,7 +358,32 @@
 			throws ReasoningMethodUnsupportedException {
 		throw new ReasoningMethodUnsupportedException();
 	}
+	
+	@Override
+	public final SortedSet<FuzzyIndividual> getFuzzyIndividuals(Description concept) {
+		reasoningStartTimeTmp = System.nanoTime();
+		SortedSet<FuzzyIndividual> result;
+		try {
+			result = getFuzzyIndividualsImpl(concept);
+		} catch (ReasoningMethodUnsupportedException e) {
+			handleExceptions(e);
+			return null;
+		}
+		nrOfRetrievals++;
+		reasoningDurationTmp = System.nanoTime() - reasoningStartTimeTmp;
+		retrievalReasoningTimeNs += reasoningDurationTmp;
+		overallReasoningTimeNs += reasoningDurationTmp;
+		if(logger.isTraceEnabled()) {
+			logger.trace("reasoner query getIndividuals: " + concept + " " + result);
+		}
+		return result;
+	}
 
+	protected SortedSet<FuzzyIndividual> getFuzzyIndividualsImpl(Description concept)
+			throws ReasoningMethodUnsupportedException {
+		throw new ReasoningMethodUnsupportedException();
+	}
+
 	@Override
 	public final boolean hasType(Description concept, Individual s) {
 		reasoningStartTimeTmp = System.nanoTime();

Modified: trunk/components-core/src/main/java/org/dllearner/core/fuzzydll/FuzzyIndividualReasoner.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/core/fuzzydll/FuzzyIndividualReasoner.java	2011-06-08 12:11:40 UTC (rev 2856)
+++ trunk/components-core/src/main/java/org/dllearner/core/fuzzydll/FuzzyIndividualReasoner.java	2011-06-08 18:10:11 UTC (rev 2857)
@@ -1,5 +1,7 @@
 package org.dllearner.core.fuzzydll;
 
+import java.util.SortedSet;
+
 import org.dllearner.core.owl.Description;
 import org.dllearner.core.owl.fuzzydll.FuzzyIndividual;
 
@@ -20,4 +22,5 @@
 	 * @return fuzzy membership degree of <code>individual</code> satisfying <code>description</code> [0-1].
 	 */
 	public double hasTypeFuzzyMembership(Description description, FuzzyIndividual individual);
+	public SortedSet<FuzzyIndividual> getFuzzyIndividuals(Description concept);
 }

Modified: trunk/components-core/src/main/java/org/dllearner/learningproblems/fuzzydll/FuzzyPosNegLPStandard.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/learningproblems/fuzzydll/FuzzyPosNegLPStandard.java	2011-06-08 12:11:40 UTC (rev 2856)
+++ trunk/components-core/src/main/java/org/dllearner/learningproblems/fuzzydll/FuzzyPosNegLPStandard.java	2011-06-08 18:10:11 UTC (rev 2857)
@@ -511,7 +511,7 @@
 		
 		// System.out.println(errorIndex++);
 
-		double crispAccuracy = crispAccuracy(description, noise);
+		// double crispAccuracy = crispAccuracy(description, noise);
 		// if I erase next line, fuzzy reasoning fails
 //		if (crispAccuracy == -1) {
 //			System.out.print(description);
@@ -525,20 +525,17 @@
 //		double posMembership = 0;
 //		double negMembership = 0;
 		double descriptionMembership = 0;
-		double singleMembership = 0;
 		// double accumulatedSingleMembership = 0;
 		double nonAccumulativeDescriptionMembership = 0;
 		double accumulativeDescriptionMembership = 0;
 		
 //		System.out.println("noise = " + noise);
 		
-		// TODO in order the noise check to work ... is it necessary to have the examples ordered by its truthBelief?
 		// int individualCounter = fuzzyExamples.size();
 		double individualCounter = totalTruth;
 		for (FuzzyIndividual fuzzyExample : fuzzyExamples) {
-			singleMembership = reasoner.hasTypeFuzzyMembership(description, fuzzyExample);
 			// accumulatedSingleMembership += singleMembership;
-			nonAccumulativeDescriptionMembership = 1 - Math.abs(fuzzyExample.getTruthDegree() - singleMembership);
+			nonAccumulativeDescriptionMembership = 1 - Math.abs(fuzzyExample.getTruthDegree() - reasoner.hasTypeFuzzyMembership(description, fuzzyExample));
 			descriptionMembership += nonAccumulativeDescriptionMembership;
 			individualCounter -= fuzzyExample.getTruthDegree();
 			if ((accumulativeDescriptionMembership + (nonAccumulativeDescriptionMembership * fuzzyExample.getTruthDegree()) + individualCounter) < ((1 - noise) * totalTruth))
@@ -552,15 +549,15 @@
 //		System.err.println("crispAccuracy = fuzzyAccuracy");
 //		crispAccuracy = fuzzyAccuracy;
 		
-		if (crispAccuracy != fuzzyAccuracy) {
-			System.err.println("***********************************************");
-			//System.err.println("* " + (errorIndex++));
-			System.err.println("* (crispAccuracy[" + crispAccuracy + "] != fuzzyAccuracy[" + fuzzyAccuracy + "])");
-			System.err.println("* DESC: " + description);
-			System.err.println("***********************************************");
-			Scanner sc = new Scanner(System.in);
-			sc.nextLine();
-		}
+//		if (crispAccuracy != fuzzyAccuracy) {
+//			System.err.println("***********************************************");
+//			//System.err.println("* " + (errorIndex++));
+//			System.err.println("* (crispAccuracy[" + crispAccuracy + "] != fuzzyAccuracy[" + fuzzyAccuracy + "])");
+//			System.err.println("* DESC: " + description);
+//			System.err.println("***********************************************");
+//			Scanner sc = new Scanner(System.in);
+//			sc.nextLine();
+//		}
 		
 		return fuzzyAccuracy;
 	}
@@ -587,7 +584,35 @@
 		}		
 		return (positiveExamples.size() - notCoveredPos + notCoveredNeg) / (double) allExamples.size();
 	}
-
+	
+	// added by Josue
+	private double crispfMeasure(Description description, double noise) {
+		// crisp F-measure
+		int additionalInstances = 0;
+		for(Individual ind : negativeExamples) {
+			if(reasoner.hasType(description, ind)) {
+				additionalInstances++;
+			}
+		}
+		
+		int coveredInstances = 0;
+		for(Individual ind : positiveExamples) {
+			if(reasoner.hasType(description, ind)) {
+				coveredInstances++;
+			}
+		}
+		
+		double recall = coveredInstances/(double)positiveExamples.size();
+		
+		if(recall < 1 - noise) {
+			return -1;
+		}
+		
+		double precision = (additionalInstances + coveredInstances == 0) ? 0 : coveredInstances / (double) (coveredInstances + additionalInstances);
+		
+		return Heuristics.getFScore(recall, precision);
+	}
+	
 	public double getFMeasureOrTooWeakExact(Description description, double noise) {
 		
 		// added by Josue
@@ -611,43 +636,19 @@
 		}
 		double fuzzyPrecision = (coveredMembershipDegree + invertedCoveredMembershipDegree) == 0 ? 0: coveredMembershipDegree / (coveredMembershipDegree + invertedCoveredMembershipDegree);
 		double fuzzyFmeasure = Heuristics.getFScore(fuzzyRecall, fuzzyPrecision);		
+
+		// double crispFmeasure = crispfMeasure(description, noise);
 		
-		// crisp F-measure
-		int additionalInstances = 0;
-		for(Individual ind : negativeExamples) {
-			if(reasoner.hasType(description, ind)) {
-				additionalInstances++;
-			}
-		}
-		
-		int coveredInstances = 0;
-		for(Individual ind : positiveExamples) {
-			if(reasoner.hasType(description, ind)) {
-				coveredInstances++;
-			}
-		}
-		
-		double recall = coveredInstances/(double)positiveExamples.size();
-		
-		if(recall < 1 - noise) {
-			return -1;
-		}
-		
-		double precision = (additionalInstances + coveredInstances == 0) ? 0 : coveredInstances / (double) (coveredInstances + additionalInstances);
-		
-//		return getFMeasure(recall, precision);
-		double crispFmeasure = Heuristics.getFScore(recall, precision);
-		
 		// crispFmeasure = fuzzyFmeasure;
 		
-		if (crispFmeasure != fuzzyFmeasure) {
-			System.err.println("************************");
-			System.err.println("* crispFmeasuer = " + crispFmeasure);
-			System.err.println("* fuzzyFmeasuer = " + fuzzyFmeasure);
-			System.err.println("************************");
-			Scanner sc = new Scanner(System.in);
-			sc.nextLine();
-		}
+//		if (crispFmeasure != fuzzyFmeasure) {
+//			System.err.println("************************");
+//			System.err.println("* crispFmeasuer = " + crispFmeasure);
+//			System.err.println("* fuzzyFmeasuer = " + fuzzyFmeasure);
+//			System.err.println("************************");
+//			Scanner sc = new Scanner(System.in);
+//			sc.nextLine();
+//		}
 
 		return fuzzyFmeasure;
 	}

Modified: trunk/components-core/src/main/java/org/dllearner/reasoning/fuzzydll/FuzzyOWLAPIReasoner.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/reasoning/fuzzydll/FuzzyOWLAPIReasoner.java	2011-06-08 12:11:40 UTC (rev 2856)
+++ trunk/components-core/src/main/java/org/dllearner/reasoning/fuzzydll/FuzzyOWLAPIReasoner.java	2011-06-08 18:10:11 UTC (rev 2857)
@@ -643,6 +643,19 @@
 	}
 	
 	@Override
+	public SortedSet<FuzzyIndividual> getFuzzyIndividualsImpl(Description concept) {
+//		OWLDescription d = getOWLAPIDescription(concept);
+		OWLClassExpression d = OWLAPIDescriptionConvertVisitor.getOWLClassExpression(concept);
+		Set<OWLNamedIndividual> individuals = reasoner.getInstances(d, false).getFlattened();
+		SortedSet<FuzzyIndividual> inds = new TreeSet<FuzzyIndividual>();
+		for(OWLNamedIndividual ind : individuals)
+			//ugly code
+			if(ind != null)
+				inds.add(new FuzzyIndividual(ind.toStringID(), this.hasTypeFuzzyMembershipImpl(concept, new FuzzyIndividual(ind.toStringID(),1))));
+		return inds;
+	}
+	
+	@Override
 	public Set<NamedClass> getTypesImpl(Individual individual) {
 		Set<Node<OWLClass>> result = null;
 		

Added: trunk/components-core/src/main/java/org/dllearner/refinementoperators/fuzzydll/FuzzyRhoDRDown.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/refinementoperators/fuzzydll/FuzzyRhoDRDown.java	                        (rev 0)
+++ trunk/components-core/src/main/java/org/dllearner/refinementoperators/fuzzydll/FuzzyRhoDRDown.java	2011-06-08 18:10:11 UTC (rev 2857)
@@ -0,0 +1,1531 @@
+/**
+ * Copyright (C) 2007-2008, Jens Lehmann
+ *
+ * This file is part of DL-Learner.
+ * 
+ * DL-Learner is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * DL-Learner is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ *
+ */
+package org.dllearner.refinementoperators.fuzzydll;
+
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.SortedSet;
+import java.util.TreeMap;
+import java.util.TreeSet;
+import java.util.Map.Entry;
+
+import org.apache.log4j.Logger;
+import org.dllearner.core.ReasonerComponent;
+import org.dllearner.core.configurators.OCELConfigurator;
+import org.dllearner.core.configurators.RefinementOperatorConfigurator;
+import org.dllearner.core.options.CommonConfigOptions;
+import org.dllearner.core.owl.BooleanValueRestriction;
+import org.dllearner.core.owl.ClassHierarchy;
+import org.dllearner.core.owl.Constant;
+import org.dllearner.core.owl.DataRange;
+import org.dllearner.core.owl.DatatypeProperty;
+import org.dllearner.core.owl.DatatypeSomeRestriction;
+import org.dllearner.core.owl.Description;
+import org.dllearner.core.owl.DoubleMaxValue;
+import org.dllearner.core.owl.DoubleMinValue;
+import org.dllearner.core.owl.Individual;
+import org.dllearner.core.owl.Intersection;
+import org.dllearner.core.owl.NamedClass;
+import org.dllearner.core.owl.Negation;
+import org.dllearner.core.owl.Nothing;
+import org.dllearner.core.owl.ObjectAllRestriction;
+import org.dllearner.core.owl.ObjectCardinalityRestriction;
+import org.dllearner.core.owl.ObjectMaxCardinalityRestriction;
+import org.dllearner.core.owl.ObjectMinCardinalityRestriction;
+import org.dllearner.core.owl.ObjectProperty;
+import org.dllearner.core.owl.ObjectPropertyExpression;
+import org.dllearner.core.owl.ObjectQuantorRestriction;
+import org.dllearner.core.owl.ObjectSomeRestriction;
+import org.dllearner.core.owl.ObjectValueRestriction;
+import org.dllearner.core.owl.StringValueRestriction;
+import org.dllearner.core.owl.Thing;
+import org.dllearner.core.owl.Union;
+import org.dllearner.core.owl.fuzzydll.FuzzyIndividual;
+import org.dllearner.refinementoperators.MathOperations;
+import org.dllearner.refinementoperators.RefinementOperatorAdapter;
+import org.dllearner.refinementoperators.Utility;
+import org.dllearner.utilities.Helper;
+import org.dllearner.utilities.owl.ConceptComparator;
+import org.dllearner.utilities.owl.ConceptTransformation;
+
+/**
+ * A downward refinement operator, which makes use of domains
+ * and ranges of properties. The operator is currently under
+ * development. Its aim is to span a much "cleaner" and smaller search
+ * tree compared to RhoDown by omitting many class descriptions,
+ * which are obviously too weak, because they violate 
+ * domain/range restrictions. Furthermore, it makes use of disjoint
+ * classes in the knowledge base.
+ * 
+ * TODO Some of the code has moved to {@link Utility} in a modified
+ * form to make it accessible for implementations of other refinement
+ * operators. These utility methods may be completed and carefully
+ * integrated back later. 
+ * 
+ * @author Jens Lehmann
+ *
+ */
+public class FuzzyRhoDRDown extends RefinementOperatorAdapter {
+
+	private static Logger logger = Logger
+	.getLogger(FuzzyRhoDRDown.class);	
+	
+	private ReasonerComponent rs;
+	
+	// hierarchies
+	private ClassHierarchy subHierarchy;
+	
+	// domains and ranges
+	private Map<ObjectProperty,Description> opDomains = new TreeMap<ObjectProperty,Description>();
+	private Map<DatatypeProperty,Description> dpDomains = new TreeMap<DatatypeProperty,Description>();
+	private Map<ObjectProperty,Description> opRanges = new TreeMap<ObjectProperty,Description>();
+	
+	// maximum number of fillers for eeach role
+	private Map<ObjectProperty,Integer> maxNrOfFillers = new TreeMap<ObjectProperty,Integer>();
+	// limit for cardinality restrictions (this makes sense if we e.g. have compounds with up to
+	// more than 200 atoms but we are only interested in atoms with certain characteristics and do
+	// not want something like e.g. >= 204 hasAtom.NOT Carbon-87; which blows up the search space
+	private int cardinalityLimit = 5;
+	
+	// start concept (can be used to start from an arbitrary concept, needs
+	// to be Thing or NamedClass), note that when you use e.g. Compound as 
+	// start class, then the algorithm should start the search with class
+	// Compound (and not with Thing), because otherwise concepts like
+	// NOT Carbon-87 will be returned which itself is not a subclass of Compound
+	private Description startClass = new Thing();
+	
+	// the length of concepts of top refinements, the first values is
+	// for refinements of \rho_\top(\top), the second one for \rho_A(\top)
+	private int topRefinementsLength = 0;
+	private Map<NamedClass, Integer> topARefinementsLength = new TreeMap<NamedClass, Integer>();
+	// M is finite and this value is the maximum length of any value in M
+	private static int mMaxLength = 4;
+	
+	// the sets M_\top and M_A
+	private Map<Integer,SortedSet<Description>> m = new TreeMap<Integer,SortedSet<Description>>();
+	private Map<NamedClass,Map<Integer,SortedSet<Description>>> mA = new TreeMap<NamedClass,Map<Integer,SortedSet<Description>>>();
+	
+	// @see MathOperations.getCombos
+	private Map<Integer, List<List<Integer>>> combos = new HashMap<Integer, List<List<Integer>>>();
+
+	// refinements of the top concept ordered by length
+	private Map<Integer, SortedSet<Description>> topRefinements = new TreeMap<Integer, SortedSet<Description>>();
+	private Map<NamedClass,Map<Integer, SortedSet<Description>>> topARefinements = new TreeMap<NamedClass,Map<Integer, SortedSet<Description>>>();
+	
+	// cumulated refinements of top (all from length one to the specified length)
+	private Map<Integer, TreeSet<Description>> topRefinementsCumulative = new HashMap<Integer, TreeSet<Description>>();
+	private Map<NamedClass,Map<Integer, TreeSet<Description>>> topARefinementsCumulative = new TreeMap<NamedClass,Map<Integer, TreeSet<Description>>>();
+	
+	// app_A set of applicable properties for a given class (separate for
+	// object properties, boolean datatypes, and double datatypes)
+	private Map<NamedClass, Set<ObjectProperty>> appOP = new TreeMap<NamedClass, Set<ObjectProperty>>();
+	private Map<NamedClass, Set<DatatypeProperty>> appBD = new TreeMap<NamedClass, Set<DatatypeProperty>>();
+	private Map<NamedClass, Set<DatatypeProperty>> appDD = new TreeMap<NamedClass, Set<DatatypeProperty>>();
+	
+	// most general applicable properties
+	private Map<NamedClass,Set<ObjectProperty>> mgr = new TreeMap<NamedClass,Set<ObjectProperty>>();
+	private Map<NamedClass,Set<DatatypeProperty>> mgbd = new TreeMap<NamedClass,Set<DatatypeProperty>>();
+	private Map<NamedClass,Set<DatatypeProperty>> mgdd = new TreeMap<NamedClass,Set<DatatypeProperty>>();
+	private Map<NamedClass,Set<DatatypeProperty>> mgsd = new TreeMap<NamedClass,Set<DatatypeProperty>>();
+	
+	// concept comparator
+	private ConceptComparator conceptComparator = new ConceptComparator();
+	
+	// splits for double datatype properties in ascening order
+	private Map<DatatypeProperty,List<Double>> splits = new TreeMap<DatatypeProperty,List<Double>>();
+	private int maxNrOfSplits = 10;
+	
+	// data structure for a simple frequent pattern matching preprocessing phase
+	private int frequencyThreshold = CommonConfigOptions.valueFrequencyThresholdDefault;
+	private Map<ObjectProperty, Map<Individual, Integer>> valueFrequency = new HashMap<ObjectProperty, Map<Individual, Integer>>();
+	// data structure with identified frequent values
+	private Map<ObjectProperty, Set<Individual>> frequentValues = new HashMap<ObjectProperty, Set<Individual>>();	
+	// frequent data values
+	private Map<DatatypeProperty, Set<Constant>> frequentDataValues = new HashMap<DatatypeProperty, Set<Constant>>();	
+	private Map<DatatypeProperty, Map<Constant, Integer>> dataValueFrequency = new HashMap<DatatypeProperty, Map<Constant, Integer>>();		
+	private boolean useDataHasValueConstructor = false;
+	
+	// staistics
+	public long mComputationTimeNs = 0;
+	public long topComputationTimeNs = 0;
+	
+	private boolean applyAllFilter = true;
+	private boolean applyExistsFilter = true;
+	private boolean useAllConstructor = true;
+	private boolean useExistsConstructor = true;
+	private boolean useHasValueConstructor = false;
+	private boolean useCardinalityRestrictions = true;
+	private boolean useNegation = true;
+	private boolean useBooleanDatatypes = true;
+	private boolean useDoubleDatatypes = true;
+	@SuppressWarnings("unused")
+	private boolean useStringDatatypes = false;
+	private boolean disjointChecks = true;
+	private boolean instanceBasedDisjoints = true;
+	
+	private boolean dropDisjuncts = false;
+
+	// caches for reasoner queries
+	private Map<Description,Map<Description,Boolean>> cachedDisjoints = new TreeMap<Description,Map<Description,Boolean>>(conceptComparator);
+
+//	private Map<NamedClass,Map<NamedClass,Boolean>> abDisjoint = new TreeMap<NamedClass,Map<NamedClass,Boolean>>();
+//	private Map<NamedClass,Map<NamedClass,Boolean>> notABDisjoint = new TreeMap<NamedClass,Map<NamedClass,Boolean>>();
+//	private Map<NamedClass,Map<NamedClass,Boolean>> notABMeaningful = new TreeMap<NamedClass,Map<NamedClass,Boolean>>();
+	
+	public FuzzyRhoDRDown(ReasonerComponent reasoningService) {
+//		this(reasoningService, reasoningService.getClassHierarchy(), null, true, true, true, true, true, 3, true, true, true, true, null);
+		this.rs = reasoningService;
+		this.subHierarchy = rs.getClassHierarchy();
+		init();
+	}
+	
+	public FuzzyRhoDRDown(ReasonerComponent reasoner, ClassHierarchy subHierarchy, Description startClass, RefinementOperatorConfigurator configurator) {
+		this.rs = reasoner;
+		this.subHierarchy = subHierarchy;
+		this.startClass = startClass;
+		useAllConstructor = configurator.getUseAllConstructor();
+		useExistsConstructor = configurator.getUseExistsConstructor();
+		useHasValueConstructor = configurator.getUseHasValueConstructor();
+		useDataHasValueConstructor = configurator.getUseDataHasValueConstructor();
+		frequencyThreshold = configurator.getValueFrequencyThreshold();
+		useCardinalityRestrictions = configurator.getUseCardinalityRestrictions();
+		cardinalityLimit = configurator.getCardinalityLimit();
+		useNegation = configurator.getUseNegation();
+		useBooleanDatatypes = configurator.getUseBooleanDatatypes();
+		useDoubleDatatypes = configurator.getUseDoubleDatatypes();
+		useStringDatatypes = configurator.getUseStringDatatypes();
+		init();
+	}
+	
+	// TODO constructor which takes a RhoDRDownConfigurator object;
+	// this should be an interface implemented e.g. by ExampleBasedROLComponentConfigurator;
+	// the goal is to use the configurator system while still being flexible enough to
+	// use one refinement operator in several learning algorithms
+	public FuzzyRhoDRDown(ReasonerComponent reasoningService, ClassHierarchy subHierarchy, OCELConfigurator configurator, boolean applyAllFilter, boolean applyExistsFilter, boolean useAllConstructor,
+			boolean useExistsConstructor, boolean useHasValueConstructor, int valueFrequencyThreshold, boolean useCardinalityRestrictions,boolean useNegation, boolean useBooleanDatatypes, boolean useDoubleDatatypes, NamedClass startClass) {
+		this.rs = reasoningService;
+		this.subHierarchy = subHierarchy;
+		this.applyAllFilter = applyAllFilter;
+		this.applyExistsFilter = applyExistsFilter;
+		this.useAllConstructor = useAllConstructor;
+		this.useExistsConstructor = useExistsConstructor;
+		this.useHasValueConstructor = useHasValueConstructor;
+		this.frequencyThreshold = valueFrequencyThreshold;
+		this.useCardinalityRestrictions = useCardinalityRestrictions;
+		cardinalityLimit = configurator.getCardinalityLimit();
+		this.useDataHasValueConstructor = configurator.getUseDataHasValueConstructor();
+		this.useNegation = useNegation;
+		this.useBooleanDatatypes = useBooleanDatatypes;
+		this.useDoubleDatatypes = useDoubleDatatypes;
+		useStringDatatypes = configurator.getUseStringDatatypes();
+		instanceBasedDisjoints = configurator.getInstanceBasedDisjoints();
+		if(startClass != null) {
+			this.startClass = startClass;
+		}
+		init();
+	}
+		
+//		subHierarchy = rs.getClassHierarchy();
+	public void init() {	
+		// query reasoner for domains and ranges
+		// (because they are used often in the operator)
+		for(ObjectProperty op : rs.getObjectProperties()) {
+			opDomains.put(op, rs.getDomain(op));
+			opRanges.put(op, rs.getRange(op));
+			
+			if(useHasValueConstructor) {
+				// init
+				Map<Individual, Integer> opMap = new TreeMap<Individual, Integer>();
+				valueFrequency.put(op, opMap);
+				
+				// sets ordered by corresponding individual (which we ignore)
+				Collection<SortedSet<Individual>> fillerSets = rs.getPropertyMembers(op).values();
+				for(SortedSet<Individual> fillerSet : fillerSets) {
+					for(Individual i : fillerSet) {
+//						System.out.println("op " + op + " i " + i);
+						Integer value = opMap.get(i);
+						
+						if(value != null) {
+							opMap.put(i, value+1);
+						} else {
+							opMap.put(i, 1);
+						}
+					}
+				}
+				
+				// keep only frequent patterns
+				Set<Individual> frequentInds = new TreeSet<Individual>();
+				for(Individual i : opMap.keySet()) {
+					if(opMap.get(i) >= frequencyThreshold) {
+						frequentInds.add(i);
+//						break;
+					}
+				}
+				frequentValues.put(op, frequentInds);
+				
+			}
+			
+		}
+		
+		for(DatatypeProperty dp : rs.getDatatypeProperties()) {
+			dpDomains.put(dp, rs.getDomain(dp));
+			
+			if(useDataHasValueConstructor) {
+				Map<Constant, Integer> dpMap = new TreeMap<Constant, Integer>();
+				dataValueFrequency.put(dp, dpMap);
+				
+				// sets ordered by corresponding individual (which we ignore)
+				Collection<SortedSet<Constant>> fillerSets = rs.getDatatypeMembers(dp).values();
+				for(SortedSet<Constant> fillerSet : fillerSets) {
+					for(Constant i : fillerSet) {
+//						System.out.println("op " + op + " i " + i);
+						Integer value = dpMap.get(i);
+						
+						if(value != null) {
+							dpMap.put(i, value+1);
+						} else {
+							dpMap.put(i, 1);
+						}
+					}
+				}
+				
+				// keep only frequent patterns
+				Set<Constant> frequentInds = new TreeSet<Constant>();
+				for(Constant i : dpMap.keySet()) {
+					if(dpMap.get(i) >= frequencyThreshold) {
+						logger.trace("adding value "+i+", because "+dpMap.get(i) +">="+frequencyThreshold);
+						frequentInds.add(i);
+					}
+				}
+				frequentDataValues.put(dp, frequentInds);				
+			}
+		}
+		
+		// we do not need the temporary set anymore and let the
+		// garbage collector take care of it
+		valueFrequency = null;
+		dataValueFrequency = null;
+		
+		// compute splits for double datatype properties
+		for(DatatypeProperty dp : rs.getDoubleDatatypeProperties()) {
+			computeSplits(dp);
+		}
+		
+		// determine the maximum number of fillers for each role
+		// (up to a specified cardinality maximum)
+		if(useCardinalityRestrictions) {
+		for(ObjectProperty op : rs.getObjectProperties()) {
+			int maxFillers = 0;
+			Map<Individual,SortedSet<Individual>> opMembers = rs.getPropertyMembers(op);
+			for(SortedSet<Individual> inds : opMembers.values()) {
+				if(inds.size()>maxFillers)
+					maxFillers = inds.size();
+				if(maxFillers >= cardinalityLimit) {
+					maxFillers = cardinalityLimit;
+					break;
+				}	
+			}
+			maxNrOfFillers.put(op, maxFillers);
+		}
+		}
+		
+		/*
+		String conceptStr = "(\"http://dl-learner.org/carcinogenesis#Compound\" AND (>= 2 \"http://dl-learner.org/carcinogenesis#hasStructure\".\"http://dl-learner.org/carcinogenesis#Ar_halide\" OR ((\"http://dl-learner.org/carcinogenesis#amesTestPositive\" IS TRUE) AND >= 5 \"http://dl-learner.org/carcinogenesis#hasBond\". TOP)))";
+		try {
+			NamedClass struc = new NamedClass("http://dl-learner.org/carcinogenesis#Compound");
+			Description d = KBParser.parseConcept(conceptStr);
+			SortedSet<Description> ds = (SortedSet<Description>) refine(d,15,null,struc);
+			System.out.println(ds);
+			
+			Individual i = new Individual("http://dl-learner.org/carcinogenesis#d101");
+			rs.instanceCheck(ds.first(), i);
+			
+		} catch (ParseException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+		System.exit(0);
+		*/
+		
+		/*
+		NamedClass struc = new NamedClass("http://dl-learner.org/carcinogenesis#Atom");
+		ObjectProperty op = new ObjectProperty("http://dl-learner.org/carcinogenesis#hasAtom");
+		ObjectSomeRestriction oar = new ObjectSomeRestriction(op,Thing.instance);
+
+		Set<Description> ds = refine(Thing.instance,3,null,struc);
+//		Set<Description> improper = new HashSet<Description>();
+		for(Description d : ds) {
+//			if(rs.subsumes(d, struc)) {
+//				improper.add(d);
+				System.out.println(d);
+//			}
+		}
+		System.out.println(ds.size());
+//		System.out.println(improper.size());
+		System.exit(0);
+		*/
+		 
+	}
+	
+	/* (non-Javadoc)
+	 * @see org.dllearner.algorithms.refinement.RefinementOperator#refine(org.dllearner.core.owl.Description)
+	 */
+	@Override
+	public Set<Description> refine(Description concept) {
+		throw new RuntimeException();
+	}
+
+	@Override
+	public Set<Description> refine(Description description, int maxLength) {
+		// check that maxLength is valid
+		if(maxLength < description.getLength()) {
+			throw new Error("length has to be at least description length (description: " + description + ", max length: " + maxLength + ")");
+		}
+		return refine(description, maxLength, null, startClass);
+	}
+	
+	/* (non-Javadoc)
+	 * @see org.dllearner.algorithms.refinement.RefinementOperator#refine(org.dllearner.core.owl.Description, int, java.util.List)
+	 */
+	@Override
+	public Set<Description> refine(Description description, int maxLength,
+			List<Description> knownRefinements) {
+		return refine(description, maxLength, knownRefinements, startClass);
+	}
+
+	@SuppressWarnings({"unchecked"})
+	public Set<Description> refine(Description description, int maxLength,
+			List<Description> knownRefinements, Description currDomain) {
+		
+//		System.out.println("|- " + description + " " + currDomain + " " + maxLength);
+		
+		// actions needing to be performed if this is the first time the
+		// current domain is used
+		if(!(currDomain instanceof Thing) && !topARefinementsLength.containsKey(currDomain))
+			topARefinementsLength.put((NamedClass)currDomain, 0);
+		
+		// check whether using list or set makes more sense 
+		// here; and whether HashSet or TreeSet should be used
+		// => TreeSet because duplicates are possible
+		Set<Description> refinements = new TreeSet<Description>(conceptComparator);
+		
+		// used as temporary variable
+		Set<Description> tmp = new HashSet<Description>();
+		
+		if(description instanceof Thing) {
+			// extends top refinements if necessary
+			if(currDomain instanceof Thing) {
+				if(maxLength>topRefinementsLength)
+					computeTopRefinements(maxLength);
+				refinements = (TreeSet<Description>) topRefinementsCumulative.get(maxLength).clone();
+			} else {
+				if(maxLength>topARefinementsLength.get(currDomain)) {
+					computeTopRefinements(maxLength, (NamedClass) currDomain);
+				}
+				refinements = (TreeSet<Description>) topARefinementsCumulative.get(currDomain).get(maxLength).clone();
+			}
+//			refinements.addAll(subHierarchy.getMoreSpecialConcepts(description));
+		} else if(description instanceof Nothing) {
+			// cannot be further refined
+		} else if(description instanceof NamedClass) {
+			refinements.addAll(subHierarchy.getSubClasses(description));
+			refinements.remove(new Nothing());
+		} else if (description instanceof Negation && description.getChild(0) instanceof NamedClass) {
+		
+			tmp = subHierarchy.getSuperClasses(description.getChild(0));
+				
+			for(Description c : tmp) {
+				if(!(c instanceof Thing))
+					refinements.add(new Negation(c));
+			}
+		
+		} else if (description instanceof Intersection) {
+				
+			// refine one of the elements
+			for(Description child : description.getChildren()) {
+				
+				// refine the child; the new max length is the current max length minus
+				// the currently considered concept plus the length of the child
+				// TODO: add better explanation
+				tmp = refine(child, maxLength - description.getLength()+child.getLength(),null,currDomain);
+				
+				// create new intersection
+				for(Description c : tmp) {
+					List<Description> newChildren = (List<Description>)((LinkedList<Description>)description.getChildren()).clone();
+					newChildren.add(c);
+					newChildren.remove(child);
+					Intersection mc = new Intersection(newChildren);
+					
+					// clean concept and transform it to ordered negation normal form
+					// (non-recursive variant because only depth 1 was modified)
+					ConceptTransformation.cleanConceptNonRecursive(mc);
+					ConceptTransformation.transformToOrderedNegationNormalFormNonRecursive(mc, conceptComparator);
+					
+					// check whether the intersection is OK (sanity checks), then add it
+					if(checkIntersection(mc))
+						refinements.add(mc);
+				}
+				
+			}
+				
+		} else if (description instanceof Union) {
+			// refine one of the elements
+			for(Description child : description.getChildren()) {
+				
+//				System.out.println("union child: " + child + " " + maxLength + " " + description.getLength() + " " + child.getLength());
+				
+				// refine child
+				tmp = refine(child, maxLength - description.getLength()+child.getLength(),null,currDomain);
+				
+				// construct intersection (see above)
+				for(Description c : tmp) {
+					List<Description> newChildren = new LinkedList<Description>(description.getChildren());
+					newChildren.remove(child);						
+					newChildren.add(c);
+					Union md = new Union(newChildren);
+						
+					// transform to ordered negation normal form
+					ConceptTransformation.transformToOrderedNegationNormalFormNonRecursive(md, conceptComparator);
+					// note that we do not have to call clean here because a disjunction will
+					// never be nested in another disjunction in this operator
+					
+					refinements.add(md);	
+				}
+				
+			}
+			
+			// if enabled, we can remove elements of the disjunction
+			if(dropDisjuncts) {
+				// A1 OR A2 => {A1,A2}
+				if(description.getChildren().size() == 2) {
+					refinements.add(description.getChild(0));
+					refinements.add(description.getChild(1));
+				} else {
+					// copy children list and remove a different element in each turn
+					for(int i=0; i<description.getChildren().size(); i++) {
+						List<Description> newChildren = new LinkedList<Description>(description.getChildren());
+						newChildren.remove(i);						
+						Union md = new Union(newChildren);
+						refinements.add(md);
+					}
+				}
+			}
+			
+		} else if (description instanceof ObjectSomeRestriction) {
+			ObjectPropertyExpression role = ((ObjectQuantorRestriction)description).getRole();
+			Description range = opRanges.get(role);
+			
+			// rule 1: EXISTS r.D => EXISTS r.E
+			tmp = refine(description.getChild(0), maxLength-2, null, range);
+
+			for(Description c : tmp)
+				refinements.add(new ObjectSomeRestriction(((ObjectQuantorRestriction)description).getRole(),c));
+			
+			// rule 2: EXISTS r.D => EXISTS s.D or EXISTS r^-1.D => EXISTS s^-1.D
+			// currently inverse roles are not supported
+			ObjectProperty ar = (ObjectProperty) role;
+			Set<ObjectProperty> moreSpecialRoles = rs.getSubProperties(ar);
+			for(ObjectProperty moreSpecialRole : moreSpecialRoles)
+				refinements.add(new ObjectSomeRestriction(moreSpecialRole, description.getChild(0)));
+
+			// rule 3: EXISTS r.D => >= 2 r.D
+			// (length increases by 1 so we have to check whether max length is sufficient)
+			if(useCardinalityRestrictions) {
+				if(maxLength > description.getLength() && maxNrOfFillers.get(ar)>1) {
+					ObjectMinCardinalityRestriction min = new ObjectMinCardinalityRestriction(2,role,description.getChild(0));
+					refinements.add(min);
+				}
+			}
+			
+			// rule 4: EXISTS r.TOP => EXISTS r.{value}
+			if(useHasValueConstructor && description.getChild(0) instanceof Thing) {
+				// watch out for frequent patterns
+				Set<Individual> frequentInds = frequentValues.get(role);
+				if(frequentInds != null) {
+					for(Individual ind : frequentInds) {
+						ObjectValueRestriction ovr = new ObjectValueRestriction((ObjectProperty)role, ind);
+						refinements.add(ovr);
+					}			
+				}
+			}
+			
+		} else if (description instanceof ObjectAllRestriction) {
+			ObjectPropertyExpression role = ((ObjectQuantorRestriction)description).getRole();
+			Description range = opRanges.get(role);
+			
+			// rule 1: ALL r.D => ALL r.E
+			tmp = refine(description.getChild(0), maxLength-2, null, range);
+
+			for(Description c : tmp) {
+				refinements.add(new ObjectAllRestriction(((ObjectQuantorRestriction)description).getRole(),c));
+			}		
+			
+			// rule 2: ALL r.D => ALL r.BOTTOM if D is a most specific atomic concept
+			if(description.getChild(0) instanceof NamedClass && tmp.size()==0) {
+				refinements.add(new ObjectAllRestriction(((ObjectQuantorRestriction)description).getRole(),new Nothing()));
+			}
+			
+			// rule 3: ALL r.D => ALL s.D or ALL r^-1.D => ALL s^-1.D
+			// currently inverse roles are not supported
+			ObjectProperty ar = (ObjectProperty) role;
+			Set<ObjectProperty> moreSpecialRoles = rs.getSubProperties(ar);
+			for(ObjectProperty moreSpecialRole : moreSpecialRoles) {
+				refinements.add(new ObjectAllRestriction(moreSpecialRole, description.getChild(0)));
+			}
+			
+			// rule 4: ALL r.D => <= (maxFillers-1) r.D
+			// (length increases by 1 so we have to check whether max length is sufficient)
+			// => commented out because this is acutally not a downward refinement
+//			if(useCardinalityRestrictions) {
+//				if(maxLength > description.getLength() && maxNrOfFillers.get(ar)>1) {
+//					ObjectMaxCardinalityRestriction max = new ObjectMaxCardinalityRestriction(maxNrOfFillers.get(ar)-1,role,description.getChild(0));
+//					refinements.add(max);
+//				}
+//			}
+		} else if (description instanceof ObjectCardinalityRestriction) {
+			ObjectPropertyExpression role = ((ObjectCardinalityRestriction)description).getRole();
+			Description range = opRanges.get(role);	
+			int number = ((ObjectCardinalityRestriction)description).getCardinality();
+			if(description instanceof ObjectMaxCardinalityRestriction) {
+				// rule 1: <= x r.C =>  <= x r.D
+				tmp = refine(description.getChild(0), maxLength-3, null, range);
+
+				for(Description d : tmp) {
+					refinements.add(new ObjectMaxCardinalityRestriction(number,role,d));
+				}				
+				
+				// rule 2: <= x r.C  =>  <= (x-1) r.C
+				ObjectMaxCardinalityRestriction max = (ObjectMaxCardinalityRestriction) description;
+//				int number = max.getNumber();
+				if(number > 1)
+					refinements.add(new ObjectMaxCardinalityRestriction(number-1,max.getRole(),max.getChild(0)));
+				
+			} else if(description instanceof ObjectMinCardinalityRestriction) {
+				tmp = refine(description.getChild(0), maxLength-3, null, range);
+
+				for(Description d : tmp) {
+					refinements.add(new ObjectMinCardinalityRestriction(number,role,d));
+				}
+				
+				// >= x r.C  =>  >= (x+1) r.C
+				ObjectMinCardinalityRestriction min = (ObjectMinCardinalityRestriction) description;
+//				int number = min.getNumber();
+				if(number < maxNrOfFillers.get(min.getRole()))
+					refinements.add(new ObjectMinCardinalityRestriction(number+1,min.getRole(),min.getChild(0)));				
+			}
+		} else if (description instanceof DatatypeSomeRestriction) {
+			
+			DatatypeSomeRestriction dsr = (DatatypeSomeRestriction) description;
+			DatatypeProperty dp = (DatatypeProperty) dsr.getRestrictedPropertyExpression();
+			DataRange dr = dsr.getDataRange();
+			if(dr instanceof DoubleMaxValue) {
+				double value = ((DoubleMaxValue)dr).getValue();
+				// find out which split value was used
+				int splitIndex = splits.get(dp).lastIndexOf(value);
+				if(splitIndex == -1)
+					throw new Error("split error");
+				int newSplitIndex = splitIndex - 1;
+				if(newSplitIndex >= 0) {
+					DoubleMaxValue max = new DoubleMaxValue(splits.get(dp).get(newSplitIndex));
+					DatatypeSomeRestriction newDSR = new DatatypeSomeRestriction(dp,max);
+					refinements.add(newDSR);
+//					System.out.println(description + " => " + newDSR);
+				}
+			} else if(dr instanceof DoubleMinValue) {
+				double value = ((DoubleMinValue)dr).getValue();
+				// find out which split value was used
+				int splitIndex = splits.get(dp).lastIndexOf(value);
+				if(splitIndex == -1)
+					throw new Error("split error");
+				int newSplitIndex = splitIndex + 1;
+				if(newSplitIndex < splits.get(dp).size()) {
+					DoubleMinValue min = new DoubleMinValue(splits.get(dp).get(newSplitIndex));
+					DatatypeSomeRestriction newDSR = new DatatypeSomeRestriction(dp,min);
+					refinements.add(newDSR);
+				}
+			}
+		} else if (description instanceof StringValueRestriction) {
+			StringValueRestriction svr = (StringValueRestriction) description;
+			DatatypeProperty dp = svr.getRestrictedPropertyExpression();
+			Set<DatatypeProperty> subDPs = rs.getSubProperties(dp);
+			for(DatatypeProperty subDP : subDPs) {
+				refinements.add(new StringValueRestriction(subDP, svr.getStringValue()));
+			}
+		}
+		
+		// if a refinement is not Bottom, Top, ALL r.Bottom a refinement of top can be appended
+		if(!(description instanceof Thing) && !(description instanceof Nothing) 
+				&& !(description instanceof ObjectAllRestriction && description.getChild(0) instanceof Nothing)) {
+			// -1 because of the AND symbol which is appended
+			int topRefLength = maxLength - description.getLength() - 1; 
+			
+			// maybe we have to compute new top refinements here
+			if(currDomain instanceof Thing) {
+				if(topRefLength > topRefinementsLength)
+					computeTopRefinements(topRefLength);
+			} else if(topRefLength > topARefinementsLength.get(currDomain))
+				computeTopRefinements(topRefLength,(NamedClass)currDomain);
+			
+			if(topRefLength>0) {
+				Set<Description> topRefs;
+				if(currDomain instanceof Thing)
+					topRefs = topRefinementsCumulative.get(topRefLength);
+				else
+					topRefs = topARefinementsCumulative.get(currDomain).get(topRefLength);
+				
+				for(Description c : topRefs) {
+					// true if refinement should be skipped due to filters,
+					// false otherwise
+					boolean skip = false;
+					
+					// if a refinement of of the form ALL r, we check whether ALL r
+					// does not occur already
+					if(applyAllFilter) {
+						if(c instanceof ObjectAllRestriction) {
+							for(Description child : description.getChildren()) {
+								if(child instanceof ObjectAllRestriction) {
+									ObjectPropertyExpression r1 = ((ObjectAllRestriction)c).getRole();
+									ObjectPropertyExpression r2 = ((ObjectAllRestriction)child).getRole();
+									if(r1.toString().equals(r2.toString()))
+										skip = true;
+								}
+							}
+						}
+					}
+					
+					// check for double datatype properties
+					/*
+					if(c instanceof DatatypeSomeRestriction && 
+							description instanceof DatatypeSomeRestriction) {
+						DataRange dr = ((DatatypeSomeRestriction)c).getDataRange();
+						DataRange dr2 = ((DatatypeSomeRestriction)description).getDataRange();
+						// it does not make sense to have statements like height >= 1.8 AND height >= 1.7
+						if((dr instanceof DoubleMaxValue && dr2 instanceof DoubleMaxValue)
+							||(dr instanceof DoubleMinValue && dr2 instanceof DoubleMinValue))
+							skip = true;
+					}*/
+					
+					// perform a disjointness check when named classes are added;
+					// this can avoid a lot of superfluous computation in the algorithm e.g.
+					// when A1 looks good, so many refinements of the form (A1 OR (A2 AND A3))
+					// are generated which are all equal to A1 due to disjointness of A2 and A3
+					if(disjointChecks && c instanceof NamedClass && description instanceof NamedClass && isDisjoint(description, c)) {
+						skip = true;
+//						System.out.println(c + " ignored when refining " + description);
+					}	
+					
+					if(!skip) {
+						Intersection mc = new Intersection();
+						mc.addChild(description);
+						mc.addChild(c);				
+						
+						// clean and transform to ordered negation normal form
+						ConceptTransformation.cleanConceptNonRecursive(mc);
+						ConceptTransformation.transformToOrderedNegationNormalFormNonRecursive(mc, conceptComparator);
+						
+						// last check before intersection is added
+						if(checkIntersection(mc))
+							refinements.add(mc);
+					}
+				}
+			}
+		}
+		
+//		for(Description refinement : refinements) {
+//			if((refinement instanceof Intersection || refinement instanceof Union) && refinement.getChildren().size()<2) {
+//				System.out.println(description + " " + refinement + " " + currDomain + " " + maxLength);
+//				System.exit(0);
+//			}
+//		}
+		
+		return refinements;		
+	}
+	
+	// when a child of an intersection is refined and reintegrated into the
+	// intersection, we can perform some sanity checks;
+	// method returns true if everything is OK and false otherwise
+	// TODO: can be implemented more efficiently if the newly added child
+	// is given as parameter
+	public static boolean checkIntersection(Intersection intersection) {
+		// rule 1: max. restrictions at most once
+		boolean maxDoubleOccurence = false;
+		// rule 2: min restrictions at most once
+		boolean minDoubleOccurence = false;
+		// rule 3: no double occurences of boolean datatypes
+		TreeSet<DatatypeProperty> occuredDP = new TreeSet<DatatypeProperty>();
+		// rule 4: no double occurences of hasValue restrictions
+		TreeSet<ObjectProperty> occuredVR = new TreeSet<ObjectProperty>();
+		
+		for(Description child : intersection.getChildren()) {
+			if(child instanceof DatatypeSomeRestriction) {
+				DataRange dr = ((DatatypeSomeRestriction)child).getDataRange();
+				if(dr instanceof DoubleMaxValue) {
+					if(maxDoubleOccurence)
+						return false;
+					else
+						maxDoubleOccurence = true;
+				} else if(dr instanceof DoubleMinValue) {
+					if(minDoubleOccurence)
+						return false;
+					else
+						minDoubleOccurence = true;
+				}		
+			} else if(child instanceof BooleanValueRestriction) {
+				DatatypeProperty dp = (DatatypeProperty) ((BooleanValueRestriction)child).getRestrictedPropertyExpression();
+//				System.out.println("dp: " + dp);
+				// return false if the boolean property exists already
+				if(!occuredDP.add(dp))
+					return false;
+			} else if(child instanceof ObjectValueRestriction) {
+				ObjectProperty op = (ObjectProperty) ((ObjectValueRestriction)child).getRestrictedPropertyExpression();
+				if(!occuredVR.add(op))
+					return false;
+			}
+//			System.out.println(child.getClass());
+		}
+		return true;
+	}
+	
+	/**
+	 * By default, the operator does not specialize e.g. (A or B) to A, because
+	 * it only guarantees weak completeness. Under certain circumstances, e.g.
+	 * refinement of a fixed given concept, it can be useful to allow such
+	 * refinements, which can be done by passing the parameter true to this method. 
+	 * @param dropDisjuncts Whether to remove disjuncts in refinement process.
+	 */
+	public void setDropDisjuncts(boolean dropDisjuncts) {
+		this.dropDisjuncts = dropDisjuncts;
+	}	
+	
+	private void computeTopRefinements(int maxLength) {
+		computeTopRefinements(maxLength, null);
+	}
+	
+	private void computeTopRefinements(int maxLength, NamedClass domain) {
+		long topComputationTimeStartNs = System.nanoTime();
+		
+		if(domain == null && m.size() == 0)
+			computeM();
+		
+		if(domain != null && !mA.containsKey(domain))
+			computeM(domain);
+		
+		int refinementsLength;
+		
+		if(domain == null) {
+			refinementsLength = topRefinementsLength;
+		} else {
+			if(!topARefinementsLength.containsKey(domain))
+				topARefinementsLength.put(domain,0);
+
+			refinementsLength = topARefinementsLength.get(domain);
+		}
+
+		// compute all possible combinations of the disjunction
+		for(int i = refinementsLength+1; i <= maxLength; i++) {
+			combos.put(i,MathOperations.getCombos(i, mMaxLength));
+
+			// initialise the refinements with empty sets
+			if(domain == null) {
+				topRefinements.put(i, new TreeSet<Description>(conceptComparator));
+			} else {
+				if(!topARefinements.containsKey(domain))
+					topARefinements.put(domain, new TreeMap<Integer,SortedSet<Description>>());
+				topARefinements.get(domain).put(i, new TreeSet<Description>(conceptComparator));
+			}
+				
+			for(List<Integer> combo : combos.get(i)) {
+				
+				// combination is a single number => try to use M
+				if(combo.size()==1) {
+					// note we cannot use "put" instead of "addAll" because there
+					// can be several combos for one length
+					if(domain == null)
+						topRefinements.get(i).addAll(m.get(i));
+					else
+						topARefinements.get(domain).get(i).addAll(mA.get(domain).get(i));
+				// combinations has several numbers => generate disjunct
+				} else {
+					
+					// check whether the combination makes sense, i.e. whether
+					// all lengths mentioned in it have corresponding elements
+					// e.g. when negation is deactivated there won't be elements of
+					// length 2 in M
+					boolean validCombo = true;
+					for(Integer j : combo) {
+						if((domain == null && m.get(j).size()==0) || 
+								(domain != null && mA.get(domain).get(j).size()==0))
+							validCombo = false;
+					}
+					
+					if(validCombo) {
+						
+						SortedSet<Union> baseSet = new TreeSet<Union>(conceptComparator);
+						for(Integer j : combo) {
+							if(domain == null)
+								baseSet = MathOperations.incCrossProduct(baseSet, m.get(j));
+							else
+								baseSet = MathOperations.incCrossProduct(baseSet, mA.get(domain).get(j));
+						}
+						
+						// convert all concepts in ordered negation normal form
+						for(Description concept : baseSet) {
+							ConceptTransformation.transformToOrderedForm(concept, conceptComparator);
+						}
+						
+						// apply the exists filter (throwing out all refinements with
+						// double \exists r for any r)
+						// TODO: similar filtering can be done for boolean datatype
+						// properties
+						if(applyExistsFilter) {
+							Iterator<Union> it = baseSet.iterator();
+							while(it.hasNext()) {
+								if(MathOperations.containsDoubleObjectSomeRestriction(it.next()))
+									it.remove();							
+							}
+						}
+							
+						// add computed refinements
+						if(domain == null)
+							topRefinements.get(i).addAll(baseSet);
+						else
+							topARefinements.get(domain).get(i).addAll(baseSet);
+						
+					}
+				}
+			}
+			
+			// create cumulative versions of refinements such that they can
+			// be accessed easily
+			TreeSet<Description> cumulativeRefinements = new TreeSet<Description>(conceptComparator);
+			for(int j=1; j<=i; j++) {
+				if(domain == null) {
+					cumulativeRefinements.addAll(topRefinements.get(j));
+				} else {
+					cumulativeRefinements.addAll(topARefinements.get(domain).get(j));
+				}
+			}			
+			
+			if(domain == null) {
+				topRefinementsCumulative.put(i, cumulativeRefinements);
+			} else {
+				if(!topARefinementsCumulative.containsKey(domain))
+					topARefinementsCumulative.put(domain, new TreeMap<Integer, TreeSet<Description>>());
+				topARefinementsCumulative.get(domain).put(i, cumulativeRefinements);
+			}
+		}
+		
+		// register new top refinements length
+		if(domain == null)
+			topRefinementsLength = maxLength;
+		else
+			topARefinementsLength.put(domain,maxLength);
+		
+		topComputationTimeNs += System.nanoTime() - topComputationTimeStartNs;
+	}
+	
+	// compute M_\top
+	private void computeM() {
+		long mComputationTimeStartNs = System.nanoTime();
+
+		// initialise all possible lengths (1 to 3)
+		for(int i=1; i<=mMaxLength; i++) {
+			m.put(i, new TreeSet<Description>(conceptComparator));
+		}
+		
+		SortedSet<Description> m1 = subHierarchy.getSubClasses(new Thing()); 
+		m.put(1,m1);		
+		
+		SortedSet<Description> m2 = new TreeSet<Description>(conceptComparator);
+		if(useNegation) {
+			Set<Description> m2tmp = subHierarchy.getSuperClasses(new Nothing());
+			for(Description c : m2tmp) {
+				if(!(c instanceof Thing)) {
+					m2.add(new Negation(c));	
+				}
+			}
+		}
+		
+		// boolean datatypes, e.g. testPositive = true
+		if(useBooleanDatatypes) {
+			Set<DatatypeProperty> booleanDPs = rs.getBooleanDatatypeProperties();
+			for(DatatypeProperty dp : booleanDPs) {
+				m2.add(new BooleanValueRestriction(dp,true));
+				m2.add(new BooleanValueRestriction(dp,false));
+			}
+		}		
+		m.put(2,m2);
+			
+		SortedSet<Description> m3 = new TreeSet<Description>(conceptComparator);
+		if(useExistsConstructor) {
+			// only uses most general roles
+			for(ObjectProperty r : rs.getMostGeneralProperties()) {
+				m3.add(new ObjectSomeRestriction(r, new Thing()));
+			}				
+		}
+		
+		if(useAllConstructor) {
+			// we allow \forall r.\top here because otherwise the operator
+			// becomes too difficult to manage due to dependencies between
+			// M_A and M_A' where A'=ran(r)
+			for(ObjectProperty r : rs.getMostGeneralProperties()) {
+				m3.add(new ObjectAllRestriction(r, new Thing()));
+			}				
+		}		
+		
+		if(useDoubleDatatypes) {
+			Set<DatatypeProperty> doubleDPs = rs.getDoubleDatatypeProperties();
+			for(DatatypeProperty dp : doubleDPs) {
+				if(splits.get(dp).size()>0) {
+					DoubleMaxValue max = new DoubleMaxValue(splits.get(dp).get(splits.get(dp).size()-1));
+					DoubleMinValue min = new DoubleMinValue(splits.get(dp).get(0));
+					m3.add(new DatatypeSomeRestriction(dp,max));
+					m3.add(new DatatypeSomeRestriction(dp,min));
+				}
+			}
+		}		
+		
+		if(useDataHasValueConstructor) {
+			Set<DatatypeProperty> stringDPs = rs.getStringDatatypeProperties();
+			for(DatatypeProperty dp : stringDPs) {
+				// loop over frequent values
+				Set<Constant> freqValues = frequentDataValues.get(dp);
+				for(Constant c : freqValues) {
+					m3.add(new StringValueRestriction(dp, c.getLiteral()));
+				}
+			}			
+		}
+		
+		m.put(3,m3);
+		
+		SortedSet<Description> m4 = new TreeSet<Description>(conceptComparator);
+		if(useCardinalityRestrictions) {
+			for(ObjectProperty r : rs.getMostGeneralProperties()) {
+				int maxFillers = maxNrOfFillers.get(r);
+				// zero fillers: <= -1 r.C does not make sense
+				// one filler: <= 0 r.C is equivalent to NOT EXISTS r.C,
+				// but we still keep it, because ALL r.NOT C may be difficult to reach
+				if(maxFillers > 0)
+					m4.add(new ObjectMaxCardinalityRestriction(maxFillers-1, r, new Thing()));
+			}			
+		}
+		m.put(4,m4);
+		
+		mComputationTimeNs += System.nanoTime() - mComputationTimeStartNs;
+	}
+	
+	// computation of the set M_A
+	// a major difference compared to the ILP 2007 \rho operator is that
+	// M is finite and contains elements of length (currently) at most 3
+	private void computeM(NamedClass nc) {
+		long mComputationTimeStartNs = System.nanoTime();
+
+//		System.out.println(nc);
+		
+		mA.put(nc, new TreeMap<Integer,SortedSet<Description>>());
+		// initialise all possible lengths (1 to 3)
+		for(int i=1; i<=mMaxLength; i++) {
+			mA.get(nc).put(i, new TreeSet<Description>(conceptComparator));
+		}
+		
+		// incomplete, prior implementation
+//		SortedSet<Description> m1 = subHierarchy.getSubClasses(nc); 
+//		mA.get(nc).put(1,m1);
+		
+		// most general classes, which are not disjoint with nc and provide real refinement
+		SortedSet<Description> m1 = getClassCandidates(nc);
+		mA.get(nc).put(1,m1);
+		
+		// most specific negated classes, which are not disjoint with nc
+		SortedSet<Description> m2 = new TreeSet<Description>();
+		if(useNegation) {
+			m2 = getNegClassCandidates(nc);
+			mA.get(nc).put(2,m2);
+		}
+		
+//		System.out.println("m1 " + "(" + nc + "): " + m1);
+//	...
 
[truncated message content]