Index: experiments/frams/logic/data/scripts/abduction_misc.inc
===================================================================
--- experiments/frams/logic/data/scripts/abduction_misc.inc	(revision 169)
+++ experiments/frams/logic/data/scripts/abduction_misc.inc	(revision 169)
@@ -0,0 +1,132 @@
+//This file contains miscellaneous support functions for the abducibles generation experiment definition. 
+//These include write-to-file function, a sorting algorithm and some combinatorial functions. 
+
+
+function writeInfo(file_name,info)
+{
+  var f=File.appendDirect("" + file_name,"description");
+  f.writeString(info);
+  f.close();
+}
+
+function quickSort(listOfNumbers,sorted)
+{
+	var l=0,r=1;
+	var stack = Vector.new();
+	stack.add(listOfNumbers);
+	while(stack.size > 0)
+	{
+		if(stack[0].size > 1)
+		{
+			while(l < r)
+			{
+				l=1;
+				r = stack[0].size - 1;
+				for(l; l < stack[0].size - 1; l++)
+					if(stack[0][0] <= stack[0][l])
+						break;
+			
+			
+			
+				for(r; r > -1; r--)
+					if(stack[0][0] > stack[0][r])
+						break;
+					
+				if(l < r)
+				{	
+					var temp_l = stack[0][l];
+					stack[0].set(l, stack[0][r]);
+					stack[0].set(r, temp_l);		
+				}
+			
+				if(l == stack[0].size - 1)
+				{
+					if(stack[0][0] > stack[0][l])
+					{
+						var temp_l = stack[0][0];
+						stack[0].set(0, stack[0][l]);
+						stack[0].set(l, temp_l);
+					}
+				}
+			}
+			var left = Vector.new();
+			var right = Vector.new();
+			var i;
+		
+			for(i = 0; i < l; i++)
+				left.add(stack[0][i]);
+			for(i = l; i < stack[0].size; i++)
+				right.add(stack[0][i]);
+		
+			stack.remove(0);
+			listInsert(stack,left,0);
+			listInsert(stack,right,1);
+			l = 0;
+			r = stack[0].size;
+		}
+		else
+		{
+			sorted.add(stack[0][0]);
+			stack.remove(0);
+		}
+	}
+	
+}
+
+function generateBinaryCombinations(size)
+{
+	var stack = Vector.new();
+	var i;
+	
+	stack.add(0);
+	var counter = 0;
+	var finish = -1;
+	var combinations = Vector.new();
+	while(stack.size > 0)
+	{
+		var z_counter = size - 1;
+		if(stack.size < size)
+		{
+			stack.add(0);
+			continue;
+		}
+		else
+		{
+			if(stack.find(1) != -1)
+			{
+				counter++;
+				var temp_bin = Vector.new();
+				for(i = 0; i < stack.size; i++)
+					temp_bin.add(stack[i]);
+					
+				combinations.add(temp_bin);		
+			}
+		}	
+		
+		if(stack.get(size - 1) == 0)
+		{
+			stack.set(size - 1, 1);
+			continue;
+		}
+			
+		if(stack.get(size - 1) == 1)
+		{
+			while(stack.get(z_counter) != 0 && z_counter > 0)
+				z_counter--;
+			
+			stack.set(z_counter, 1);
+			
+			while(z_counter != (stack.size - 1))
+				stack.remove(stack.size - 1);
+				
+			if(stack.get(0) == 1 && stack.size == 1)
+				
+				finish++;
+				
+				if(finish == 1)
+					stack.clear();
+			
+		}	
+	}
+	return combinations;
+}
Index: experiments/frams/logic/data/scripts/data_conversion.inc
===================================================================
--- experiments/frams/logic/data/scripts/data_conversion.inc	(revision 169)
+++ experiments/frams/logic/data/scripts/data_conversion.inc	(revision 169)
@@ -0,0 +1,258 @@
+//This file contains data conversion functions such as index-encoding-to-human-readible-format function, prefix-to-infix-format conversion function,
+//formula-to-latex converters, etc...  
+
+
+function binaryToIndex(binaryCombination, baseHypothesesIndexed)
+{
+	
+	if(binaryCombination.find(1) == -1)
+		return null;
+	
+	var hypothesis = Vector.new();
+	var first = binaryCombination.find(1);
+	hypothesis = getIndexedConjunctionFromLiterals(baseHypothesesIndexed[first]);
+	var i;
+	
+	for(i = first + 1; i < binaryCombination.size; i++)
+	{
+		if(binaryCombination[i] == 1)
+		{
+			hypothesis = (plainListCopyInsert(mergePlainLists(hypothesis, getIndexedConjunctionFromLiterals(baseHypothesesIndexed[i])), 0, [2]));
+		}
+	}
+	
+	return hypothesis;
+}
+
+
+function binaryToForm(binaryCombinations, baseHypotheses)
+{
+	
+	if(binaryCombinations.find(1) == -1)
+		return null;
+	
+	var hypothesis = "";
+	
+	var first = binaryCombinations.find(1);
+	hypothesis = baseHypotheses[first];
+	var i;
+	
+	for(i = first + 1; i < binaryCombinations.size; i++)
+	{
+		if(binaryCombinations[i] == 1)
+		{
+			hypothesis = "A" + hypothesis + baseHypotheses[i];
+		}
+	}
+	
+	return hypothesis;
+}
+
+function convertIndexedSetToLatex(listOfIndexedForms)
+{
+	
+	var i;
+	var setLatex = "\\{";
+	var litLatex = "";
+	var allLatex = "";
+	for(i = 0; i < listOfIndexedForms.size; i++)
+	{		
+			var infix = Vector.new();
+			infix = indexesPrefixToInfix(listOfIndexedForms[i], infix);
+			var formInfix = createInfixFormFromIndexesInfix(infix);
+			var latex = formToLatex(formInfix);
+			
+			if(i < (listOfIndexedForms.size - 2))
+				setLatex += latex + ", ";
+			else if(i == (listOfIndexedForms.size - 2))
+					setLatex += latex;
+				 else if(i == (listOfIndexedForms.size - 1))
+						litLatex = latex;
+						
+	}
+		if(setLatex != "\\{")
+			allLatex = setLatex + ", " + litLatex + "\\}";
+		else
+			allLatex = setLatex + litLatex + "\\}";
+		
+		return allLatex;
+}
+
+function formToLatex(form)
+{
+	var i;
+	var len = String.len(form);
+	
+	var newForm = String.replace(form, "A", " \\lor ");
+		newForm = String.replace(newForm, "K", " \\land ");
+		newForm = String.replace(newForm, "C", " \\to ");
+		newForm = String.replace(newForm, "E", " \\equiv ");
+		newForm = String.replace(newForm, "N", " \\lnot ");
+				
+	return newForm;
+}
+
+function createInfixFormFromIndexesInfix(indexesInfix)
+{
+	var form = "";
+	var i;
+	var symbolType = 0;
+	for(i = 0; i < indexesInfix.size; i++)
+	{
+		symbolType = typeof(indexesInfix[i]);
+		if(symbolType != 0)
+		{
+			if(symbolType == 3)
+			{
+				form += indexesInfix[i];
+			}
+			else
+			{
+				form += g_symbolsChart[indexesInfix[i]];
+			}
+		}
+		else
+			return Simulator.print("There is a problem with symbols in the indexed infix form!");
+	}
+	
+	return form;
+}
+
+function indexesPrefixToInfix(listOfIndexes, infix)
+{
+	var symbol = listOfIndexes[0];
+		
+	if((symbol == 1) || (symbol == 2) || (symbol == 3))
+	{
+			var args = getIndexedMainArgs(listOfIndexes);
+			infix.add("(");
+			infix = indexesPrefixToInfix(args[0],infix);
+			infix.add(symbol);
+			infix = indexesPrefixToInfix(args[1], infix);
+			infix.add(")");
+			return infix;
+	}
+	else
+	{
+		if(symbol == 0)
+		{
+			infix.add(symbol);
+			var args = getIndexedMainArgs(listOfIndexes);
+			infix = indexesPrefixToInfix(args[0], infix);
+			return infix;
+		}
+		else
+		{
+			infix.add(symbol);
+			return infix;
+		}
+	}
+}
+
+function getIndexedConjunctionFromLiterals(indexedListOfLiterals)
+{
+	var i,j;
+	var result = Vector.new();
+	
+	
+	
+	for(j = 0; j < indexedListOfLiterals[0].size; j++)
+		result.add(indexedListOfLiterals[0][j]);
+	
+	for(i = 1; i < indexedListOfLiterals.size; i++)
+	{
+		result = plainListCopyInsert(result, 0, [1]);
+		for(j = 0; j < indexedListOfLiterals[i].size; j++)
+			result.add(indexedListOfLiterals[i][j]);
+		
+	}
+	
+	return result;
+}
+
+function formulaFromLiterals(literals)
+{
+	var i,j;
+	var form = convertIndexesToForm(literals[0]);
+	
+	
+	for(i = 1; i < literals.size; i++)
+		form = "K" + form + convertIndexesToForm(literals[i]);
+		
+	return form;
+}
+
+function convertIndexesToForm(setOfIndexes)
+{
+	var form = "";
+	var i;
+	
+	for(i = 0; i < setOfIndexes.size; i++)
+	{
+		form += g_symbolsChart[setOfIndexes[i]];	
+	}
+	
+	return form;
+}
+
+function getFormListFromIndexes(literalsListsIndexed)
+{
+	var i,j;
+	var new = Vector.new();
+	for(i = 0; i < literalsListsIndexed.size; i++)
+	{
+		new.add(Vector.new());
+		
+		for(j = 0; j < literalsListsIndexed[i].size; j++)
+			new[i].add(convertIndexesToForm(literalsListsIndexed[i][j]));
+	}
+	
+	return new;
+}
+
+function convertLiteralsToNumbers(setOfLiteralsIndexed)
+{
+	var i;
+	var result = Vector.new();
+	
+	for(i = 0; i < setOfLiteralsIndexed.size; i++)
+	{
+		if(setOfLiteralsIndexed[i].size > 0 && setOfLiteralsIndexed[i].size < 3)
+		{
+			if(setOfLiteralsIndexed[i][0] == 0)
+				result.add(setOfLiteralsIndexed[i][1]);
+			else
+				result.add(100+setOfLiteralsIndexed[i][0]);
+		}
+		else
+		{
+			Simulator.print("There is a problem with entangled literals!");
+		}
+	}
+	return result;
+}
+
+function convertNumbersToLiterals(setOfNumbers)
+{
+	var i;
+	var result = Vector.new();
+	
+	for(i = 0; i < setOfNumbers.size; i++)
+	{
+		if(setOfNumbers[i] != 0)
+		{
+			if(setOfNumbers[i] < 100)
+			{
+				result.add([0,setOfNumbers[i]]);
+			}
+			else
+			{
+				result.add([setOfNumbers[i]%100]);
+			}
+		}
+		else
+			Simulator.print("There is a problem with entangled literals!");
+	}
+	
+	return result;
+}
Index: experiments/frams/logic/data/scripts/formulas_processing.inc
===================================================================
--- experiments/frams/logic/data/scripts/formulas_processing.inc	(revision 169)
+++ experiments/frams/logic/data/scripts/formulas_processing.inc	(revision 169)
@@ -0,0 +1,121 @@
+//This file contains formulas processing functions such as subformulas and variables ``getters''.
+
+function getSubFormulasIndexed(formInd)
+{
+	var i;
+	var stack = Vector.new();
+	var setOfSubforms = Vector.new();
+	setOfSubforms.add(formInd);
+	if(formInd[0] < 4)
+	{
+		stack = getIndexedMainArgs(formInd);
+		for(i = 0; i < stack.size; i++)
+		{
+			if(findPlainList(setOfSubforms, stack[i]) == -1)
+				setOfSubforms.add(stack[i]);
+		}
+	}
+
+	while(stack.size > 0)	
+	{
+		if(stack[0][0] < 4)
+		{	
+			var tempForms = Vector.new();
+			tempForms = getIndexedMainArgs(stack[0]);
+			for(i = 0; i < tempForms.size; i++)
+			{
+				if(findPlainList(setOfSubforms, tempForms[i]) == -1)
+				{
+					setOfSubforms.add(tempForms[i]);
+					stack.add(tempForms[i]);
+				}
+			}
+		}
+		stack.remove(0);
+	}
+	
+	return setOfSubforms;
+}
+
+function getVariablesIndexed(setOfSubforms)
+{
+	var i;
+	var variables = Vector.new();
+	
+	for(i = 0; i < setOfSubforms.size; i++)
+		if(setOfSubforms[i][0] > 3 && variables.find(setOfSubforms[i]) == -1)
+			variables.add(setOfSubforms[i]);
+	
+	
+	return variables;
+}
+
+function getIndexedMainArgs(formInd)
+{
+	
+	var argsList = Vector.new();
+	if(formInd[0] > 0 && formInd[0]  < 4)
+	{
+ 		var firstArgStart = Vector.new();
+ 		firstArgStart.add(formInd[1]);
+ 		var firstArg = Vector.new();
+ 		var secondArg = Vector.new();
+ 		
+ 		
+ 		if(firstArgStart[0] > 3)
+ 		{
+ 			argsList.add(firstArgStart);
+ 			secondArg = plainListRight(formInd, formInd.size - 2);
+ 			argsList.add(secondArg);
+ 		}
+ 		else
+ 		{
+ 			var i;
+ 			var p = 2, p_temp = 2, e = 1;
+ 			var check_conj = 1;
+
+ 			
+ 			while(check_conj == 1)
+ 			{	
+ 				for(i = e; i < p; i++)
+ 				{
+ 					if(formInd[i] == 0)
+ 					{
+ 						p_temp++;
+ 					}
+ 					if(formInd[i] > 0 && formInd[i] < 4)
+ 					{
+ 						p_temp += 2;
+ 					}	
+ 				}
+ 				
+ 				if(p == p_temp)
+ 					check_conj = 0;
+ 						
+ 				e = p;
+ 				p = p_temp;	
+ 			}
+ 				
+ 			firstArg = plainListSubList(formInd, 1, p - 1);
+ 			argsList.add(firstArg);
+ 			secondArg = plainListRight(formInd, formInd.size - p);
+ 			argsList.add(secondArg);
+ 		}
+ 		
+		return argsList;
+	}
+	else
+	{
+		if(formInd[0] == 0)
+		{
+			argsList.add(plainListRight(formInd, formInd.size - 1));
+			return argsList;
+		}
+		else
+		{
+			Simulator.print("There is no proper operator");
+			return Vector.new();
+		}
+	}
+	
+}
Index: experiments/frams/logic/data/scripts/lists_processing.inc
===================================================================
--- experiments/frams/logic/data/scripts/lists_processing.inc	(revision 169)
+++ experiments/frams/logic/data/scripts/lists_processing.inc	(revision 169)
@@ -0,0 +1,196 @@
+//This file contains list manipulation functions.
+
+function verifyPlainListsIdentity(list1, list2)
+{
+	
+	if(list1.size != list2.size)
+		return 0;
+	else
+	{
+		var i;
+		
+		for(i = 0; i < list1.size; i++)
+		{
+			if(list1[i] != list2[i])
+				return 0;
+		}
+		
+		return 1;
+				
+	}
+}
+
+function findPlainList(vector, list)
+{
+	var i;
+	
+	for(i = 0; i < vector.size; i++)
+	{
+		if(verifyPlainListsIdentity(vector[i], list) == 1)
+			return i;
+	}
+	
+	return -1;
+}
+
+function copyPlainList(list)
+{
+	var i;
+	var newList = Vector.new();
+	
+	for(i = 0; i < list.size; i++)
+		newList.add(list[i]);
+		
+	return newList;
+}
+
+function deepCopyList(arg)
+{
+  if (typeof(arg) == "Vector")
+  {
+    var i, v = Vector.new();
+    for (i = 0;i < arg.size;i++)
+      v.add(deepCopyList(arg[i]));
+    return v;
+  }
+  else
+    return arg;
+}
+
+function plainListRight(list, howMany)
+{
+	var right = Vector.new();
+	var i;
+	
+	for(i = list.size-howMany; i < list.size; i++)
+		right.add(list[i]);
+	
+	return right;
+}
+
+function plainListLeft(list, howMany)
+{
+	var left = Vector.new();
+	var i;
+	
+	for(i = 0; i <= howMany; i++)
+	{
+		left.add(list[i]);
+	}
+	
+	return left;
+}
+
+function plainListSubList(list, start, stop)
+{
+	var i;
+	var subList = Vector.new();
+	
+	for(i = start; i <= stop; i++)
+	{
+		subList.add(list[i]);
+	}
+	
+	return subList;
+}
+
+function plainListReplace(list, index, replaceList)
+{
+	var new = Vector.new();
+	var i;
+	
+	for(i = 0; i < index; i++)
+	{
+		new.add(list[i]);
+	}
+	
+	for(i = 0; i < replaceList.size; i++)
+	{
+		new.add(replaceList[i]);
+	}
+	
+	for(i = index + 1; i < list.size; i++)
+	{
+		new.add(list[i]);
+	}
+	
+	return new;
+	
+}
+
+function mergePlainLists(list1, list2)
+{
+	var i;
+	var new = Vector.new();
+	
+	for(i = 0; i < list1.size; i++)
+		new.add(list1[i]);
+		
+	for(i = 0; i < list2.size; i++)
+		new.add(list2[i]);
+		
+	return new;
+}
+
+function plainListCopyInsert(list, index, elementsList)
+{
+	var new = Vector.new();
+	var i;
+	
+	for(i = 0; i < index; i++)
+	{
+		new.add(list[i]);
+	}
+	
+	for(i = 0; i < elementsList.size; i++)
+	{
+		new.add(elementsList[i]);
+	}
+	
+	for(i = index; i < list.size; i++)
+	{
+		new.add(list[i]);
+	}
+	
+	return new;
+}
+
+function listRemove(indexes, list)
+{
+	var listDeepCopy = deepCopyList(list);
+	
+	var i;
+	
+	for(i = 0; i < indexes.size; i++)
+	{
+		listDeepCopy.set(indexes[i],null);
+	}
+	
+	for(i = 0; i < listDeepCopy.size; i++)
+		if(listDeepCopy[i] == null)
+		{
+			listDeepCopy.remove(i);
+			i--;
+		}
+		
+	return listDeepCopy;
+}
+
+function listInsert(list,element,position)
+{
+	if(position >= list.size)
+		list.set(position, element);
+	else
+	{
+		var temp = Vector.new();
+		var i;
+		for(i = position; i < list.size; i++)
+			temp.add(list[i]);
+			
+		list.set(position,element);
+		
+		for(i = 0; i < temp.size; i++)
+			list.set(position + 1 + i,temp[i]);
+	}
+	
+}
Index: experiments/frams/logic/data/scripts/literals_processing.inc
===================================================================
--- experiments/frams/logic/data/scripts/literals_processing.inc	(revision 169)
+++ experiments/frams/logic/data/scripts/literals_processing.inc	(revision 169)
@@ -0,0 +1,392 @@
+//This file contains literals processing functions such as: entangled literals ``get'' function,
+//literals clauses sorting, reduction and filtering functions.
+
+
+function getEntangledLiterals(inferencesIndexed, formulasIndexed)
+{
+	var i,j,l;
+	var k = 0;
+	var entangledLiterals = Vector.new();
+	
+	for(i = 0; i < inferencesIndexed.size; i++)
+	{
+		entangledLiterals.add(Vector.new());
+		while(k < formulasIndexed.size)
+		{
+			for(j = 1; j < inferencesIndexed[i].size; j++)
+			{
+				var negFormIndexed = plainListCopyInsert(formulasIndexed[k], 0, [0]);
+				if(verifyPlainListsIdentity(inferencesIndexed[i][j][0], formulasIndexed[k]) || verifyPlainListsIdentity(inferencesIndexed[i][j][0], negFormIndexed))
+				{
+					for(l = 0; l < inferencesIndexed[i][j][1].size; l++)
+						entangledLiterals[i].add(deepCopyList(inferencesIndexed[i][j][1][l]));
+					
+					continue;
+				}
+			}
+			k++;
+		}
+		k = 0;
+	}
+	return entangledLiterals;
+}
+
+
+function cleanEntangledLiterals(entangledLiterals)
+{
+	var i,j,k;
+	var cleaned = Vector.new();
+	var check = 0;
+	var tempEntangled = Vector.new();
+	
+	for(i = 0; i < entangledLiterals.size; i++)
+	{
+		tempEntangled.add(Vector.new());
+		
+		for(j = 0; j < entangledLiterals[i].size; j++)
+			if(findPlainList(tempEntangled[tempEntangled.size - 1], (entangledLiterals[i][j])) == -1)
+				tempEntangled[tempEntangled.size - 1].add(entangledLiterals[i][j]);
+	}
+	
+	cleaned.add(tempEntangled[0]);
+	for(i = 1; i < tempEntangled.size; i++)
+	{
+		
+		check = 0;
+		for(j = 0; j < cleaned.size; j++)
+		{
+			if(tempEntangled[i].size != cleaned[j].size)
+				continue;
+			else		
+				for(k = 0; k < tempEntangled[i].size; k++)
+					if(findPlainList(cleaned[j], tempEntangled[i][k]) == -1)
+						continue 2;
+						
+			check = 1;		
+		}
+		if(check == 0)
+			cleaned.add(tempEntangled[i]);
+	}
+	return cleaned;
+}
+
+function filterOutNonConsistentLiteralsLists(listsOfLiterals)
+{
+	var i,j,k;
+	var result = Vector.new();
+	for(i = 0; i < listsOfLiterals.size; i++)
+	{
+		for(j = 0; j < listsOfLiterals[i].size; j++)
+		{
+			for(k = j+1; k < listsOfLiterals[i].size; k++ )
+			{
+				if(verifyPlainListsIdentity(listsOfLiterals[i][j],  plainListCopyInsert(listsOfLiterals[i][k], 0, [0])) == 1 || verifyPlainListsIdentity(plainListCopyInsert(listsOfLiterals[i][j], 0, [0]), listsOfLiterals[i][k]) == 1)
+					continue 3;
+			}	
+		}
+		result.add(listsOfLiterals[i]);
+	}
+	return result;
+}
+
+function filterOutRepeatingLiteralsLists(listsOfLiterals)
+{
+	var result = Vector.new();
+	var i,j,k;
+	
+	for(i = 0; i < listsOfLiterals.size; i++)
+	{
+		for(j = 0; j < result.size; j++)
+		{
+			if(listsOfLiterals[i].size == result[j].size)
+			{
+				
+				for(k = 0; k < listsOfLiterals[i].size; k++)
+				{
+					if(verifyPlainListsIdentity(listsOfLiterals[i][k], result[j][k]) == 0)
+						continue 2;
+					
+				}
+				continue 2;
+			}
+			else
+				continue;
+		}
+		result.add(deepCopyList(listsOfLiterals[i]));
+	}
+	
+	return result;
+}
+
+
+function getSymmetricalDifferences(literalsSets)
+{
+	var literalsSetsDeepCopy = deepCopyList(literalsSets);
+	
+	var i,j;
+	var mem = 0;
+	var indexMem = Vector.new();
+	var ijs = Vector.new();
+	
+	for(i = 0; i < literalsSetsDeepCopy.size; i++)
+	{
+		mem = 0;
+		
+		for(j=0; j < literalsSetsDeepCopy.size; j++)
+		{
+			if(i!=j)
+			{	
+				var tempIjs = Vector.new();
+				if(i > j)
+				{
+					tempIjs.add(j);
+					tempIjs.add(i);	
+				}
+				else
+				{
+					tempIjs.add(i);
+					tempIjs.add(j);	
+				}
+				if((literalsSetsDeepCopy[i].size == literalsSetsDeepCopy[j].size)  && (findPlainList(ijs, tempIjs) == -1))
+				{
+					ijs.add(tempIjs);
+					var sd = symDiffOfTwoLiteralsSets(literalsSetsDeepCopy[i], literalsSetsDeepCopy[j]);
+					if(sd[0] != null)
+					{
+						mem = 1;
+						literalsSetsDeepCopy.add(sd);
+						if(indexMem.find(j) == -1)
+							indexMem.add(j);
+					}
+				}
+			}	
+		}
+		
+		if(mem == 1)
+		{
+			if(indexMem.find(i)==-1)
+				indexMem.add(i);
+			
+		}
+	}
+	var remliteralsSetsDeepCopy = listRemove(indexMem, literalsSetsDeepCopy);
+	return remliteralsSetsDeepCopy;
+}
+
+
+function symDiffOfTwoLiteralsSets(set1, set2)
+{
+	
+	if(set1.size==set2.size)
+	{
+		var i;
+		var candidateSet = deepCopyList(set1);
+		
+		var j;
+		var diffCounter = 0;	
+		for(j = 0; j < set2.size; j++)
+		{
+			if(findPlainList(candidateSet, set2[j]) == -1)
+			{
+				if(set2[j].size == 2)
+				{
+					var find = findPlainList(candidateSet, [set2[j][1]]);
+						if(find != -1)
+						{
+							diffCounter++;
+							candidateSet.remove(find);
+						}
+						else
+							return [null];
+				}
+				else if(set2[j].size == 1)
+					 {
+					 	var find = findPlainList(candidateSet, plainListCopyInsert(set2[j], 0, [0]));
+					 	if(find != -1)
+						{
+							diffCounter++;
+							candidateSet.remove(find);
+						}
+						else
+							return [null];
+					 }	
+			}
+			
+			if(diffCounter > 1)
+				return [null];	
+		}
+		if(diffCounter == 0)
+			return [null];
+		
+		if(diffCounter==1)
+			return candidateSet;
+	}
+	else
+	{
+		Simulator.print("The compared sets of literals are of different sizes!");
+		return [null];
+	}
+}
+
+function removeLiteralsSupSets(setsOfLiterals)
+{
+	var i;
+	
+	var sorted = sortLiteralsListsBySize(setsOfLiterals);
+	for(i = sorted.size - 1; i > -1; i--)
+	{
+		var j;
+		for(j = i - 1; j > -1; j--)
+		{
+
+			if(sorted[i].size > sorted[j].size)
+			{
+				var k;
+				
+				for(k = 0; k < sorted[j].size; k++)
+				{
+					if(findPlainList(sorted[i], sorted[j][k]) == -1)
+						continue 2;
+					
+				}
+				sorted.remove(i);
+				continue 2;
+			}
+			
+		}
+	}
+	return sorted;
+}
+
+
+function generateBaseHypotheses(entangledLiterals)
+{
+	var i;
+	var literalsCounter = 0;
+	var stack = Vector.new();
+	var product = Vector.new();
+	var tempLiteral = Vector.new();
+	var check = 0;
+	
+	while(!(stack.size == 0 && literalsCounter == entangledLiterals[0].size))
+	{ 
+		tempLiteral = deepCopyList(entangledLiterals[stack.size][literalsCounter]);
+		
+		if(tempLiteral[0] != 0)
+			tempLiteral = plainListCopyInsert(tempLiteral, 0, [0]);
+		else
+			tempLiteral = [tempLiteral[1]];
+		
+		for(i = 0; i < stack.size; i++)
+		{	
+			if(stack[i][1] != null)
+			if(verifyPlainListsIdentity(stack[i][1], tempLiteral) == 1)	
+			{
+				stack.add([literalsCounter, null]);
+				check = 1;
+				break;
+			}	
+		}
+		if(check == 0)
+		{
+			stack.add([literalsCounter, tempLiteral]);
+		}
+		else
+			check = 0;	
+	
+		if(stack.size == entangledLiterals.size)	
+		{	
+			product.add(Vector.new());
+			
+			for(i = 0; i < stack.size; i++)
+			{
+				if(stack[i][1] != null)
+					product[product.size - 1].add(stack[i][1]);
+				else
+					continue;
+			}
+			
+			literalsCounter = stack[stack.size - 1][0] + 1;
+			stack.remove(stack.size - 1);
+				
+			if(literalsCounter == entangledLiterals[stack.size].size)
+			{
+				if(stack.size != 0)
+				{
+					literalsCounter = stack[stack.size - 1][0] + 1;
+					while(stack.size != 0 && literalsCounter == entangledLiterals[stack.size - 1].size)
+					{
+						stack.remove(stack.size - 1);
+			
+						if(stack.size > 0)
+							literalsCounter = stack[stack.size - 1][0] + 1;
+						else
+							break;
+					}
+					if(stack.size > 0)
+						stack.remove(stack.size - 1);
+				}
+			}
+		}
+		else
+			literalsCounter = 0;
+	}
+	
+	return product;
+}
+
+
+
+function sortLiteralsListsBySize(literalsLists)
+{
+	var i;
+	var ranks = Vector.new();
+	var numbers = Vector.new();
+	var ordered = Vector.new();
+	
+	for(i = 0; i < literalsLists.size; i++)
+	{
+		var count = literalsLists[i].size;
+		numbers.add(count);
+		ranks.add([count,i]);
+	}
+	var sorted = Vector.new();
+	quickSort(numbers,sorted);
+	while(sorted.size > 0)
+	{
+		for(i = 0; i < ranks.size; i++)
+			if(sorted[0] == ranks[i][0])
+			{
+				ordered.add(literalsLists[ranks[i][1]]);
+				sorted.remove(0);
+				ranks.remove(i);
+				break;
+			}
+	}
+	return ordered;
+}
+
+function sortLiteralsWithinSets(setOfLiteralsSetsIndexed)
+{
+	var new = Vector.new();
+	var i;
+	
+	for(i = 0; i < setOfLiteralsSetsIndexed.size; i++)
+		new.add(sortLiterals(setOfLiteralsSetsIndexed[i]));
+		
+	return new;
+}
+
+function sortLiterals(setOfLiterals)
+{
+	var numeric = Vector.new();
+	var sortedNum = Vector.new();
+	var sortedLiterals = Vector.new();
+	var i;
+	
+	numeric = convertLiteralsToNumbers(setOfLiterals);
+	quickSort(numeric,sortedNum);
+	sortedLiterals = convertNumbersToLiterals(sortedNum);
+	
+	return sortedLiterals;
+}
Index: experiments/frams/logic/data/scripts/logic_abduction.expdef
===================================================================
--- experiments/frams/logic/data/scripts/logic_abduction.expdef	(revision 169)
+++ experiments/frams/logic/data/scripts/logic_abduction.expdef	(revision 169)
@@ -0,0 +1,259 @@
+expdef:
+name:Generate abductive hypotheses
+info:~
+This experiment definition generates abducibles for a specified abductive problem.
+
+Results and details are published in Transactions on Computational Logic, 2014,
+"Identifying efficient abductive hypotheses using multi-criteria dominance relation"
+by M. Komosinski, A. Kups, D. Leszczynska-Jasion and M. Urbanski.
+
+See also readme-abduction.txt and run-abduction.cmd.
+~
+code:~
+
+global g_params;
+global g_form;
+global g_set;
+global g_file;
+global g_symbolsChart;
+global g_oldSymbolsChart;
+
+function onExpDefLoad()
+{
+  GenePools.clear();
+  Populations.clear();
+  Populations[0].clear();
+ 
+  Math.randomize();
+	
+	
+	var g_params = Vector.new();
+	
+	//Logical symbols chart including up to nine distinct variables
+	g_symbolsChart = ["N", "K", "A", "C", "p", "q", "r", "s", "t", "u", "v", "w", "x"];
+	
+	g_form = Vector.new();
+	g_set = Vector.new();
+	g_file = "";	
+
+}
+
+
+function onExpInit()
+{
+	//Initialization of the experiment parameters loaded from file
+	g_params = String.split(ExpParams.params, ";");
+	if(g_params.size == 3)
+	{
+		//Conversion of the string characters into a numerical encoding
+		var i,j;
+		var splitedForm = String.split(g_params[0],"_");
+		
+		for(i = 0; i < splitedForm.size; i++)
+		{
+			g_form.add(g_symbolsChart.find(splitedForm[i]));
+		}
+		
+		var splitedSet = String.split(g_params[1], " ");
+		var splitedElt = Vector.new();
+		
+		for(i = 0; i < splitedSet.size; i++)
+		{
+			g_set.add(Vector.new());
+			splitedElt = String.split(splitedSet[i], "_");	
+		
+			for(j = 0; j < splitedElt.size; j++)
+			{
+				g_set[i].add(g_symbolsChart.find(splitedElt[j]));
+			}
+		}
+		
+		g_file = g_params[2];
+		
+	} else
+	  {
+		Simulator.print("Something is not right with the experiment parameters!");
+	  }
+	  
+}
+
+function onStep()
+{
+	if(g_params.size == 3)
+	{
+		//Call of the main function of the experiment
+		getRawHypotheses(g_set, g_form, g_file);
+		Simulator.stop();
+	} else
+	  {
+		Simulator.print("Something is wrong with experiment parameters! Stopping simulation...");
+		Simulator.stop();
+	  }
+}
+
+//Main function of the experiment
+function getRawHypotheses(set, form, fileName)
+{
+		var i,j;
+		//Generation of the list containg all the formulas of the problem
+		var formulas = Vector.new();
+		for(i = 0; i < set.size; i++)
+			formulas.add(set[i]);
+		
+		formulas.add(form);	
+		//Generation of the list containing all the subformulas of the problem
+		var subformulas = Vector.new();
+		for(i = 0; i < formulas.size; i++)
+		{
+		
+			var tempSf = getSubFormulasIndexed(formulas[i]);
+			for(j = 0; j < tempSf.size; j++)
+			{
+				if(findPlainList(subformulas, tempSf[j]) == -1)
+					subformulas.add(tempSf[j]);
+			}
+			
+		}
+	
+		//Generation of the list containing all the variables of the problem
+		var variables = getVariablesIndexed(subformulas);
+		
+		//Generation of the synthetic inferences list
+		var inferences = generateSyntheticInfFromSetIndexed(formulas, subformulas, variables);
+		
+		//Checking whether a tableau is closed
+		var success = checkTableauSuccess(inferences, formulas);
+		if(!success)
+		{
+			//Generation of the output file name
+			var fileNSplit = String.split(fileName, ".");
+			var  fName = fileNSplit[0] + "RawHyp.txt";
+			
+			//Generation and preprocessing list of the abductive hypotheses
+			rawHypothesesGeneration(inferences, set, form, formulas, fName);
+			
+	
+		} else
+		  {
+			//Printing out of the output if the table is closed
+			var setLatex = convertIndexedSetToLatex(set);
+			var infix = Vector.new();
+			infix = indexesPrefixToInfix(form, infix);
+			var formInfix = createInfixFormFromIndexesInfix(infix);
+			var formLatex = formToLatex(formInfix);
+			
+			writeInfo(fileName, "#set: " + setLatex + "	form: " + formLatex + "\n");
+			writeInfo(fileName, "success\n");
+		  }
+		  
+}
+
+function rawHypothesesGeneration(inferences, set, form, formulas, file_name)
+{
+	
+	var valid = checkTableValidity(inferences, formulas);
+	
+	//Function that gets failure inferences
+	var partialTableaux = getFailures(inferences, formulas);
+	var partialTableau = partialTableaux[0];
+	
+	//Functions that get and reduce entangled literals clauses
+	var entangledLiterals = getEntangledLiterals(partialTableau, formulas);
+	var entangledHuman = getFormListFromIndexes(entangledLiterals);
+	var cleaned = cleanEntangledLiterals(entangledLiterals);
+	var cleanedHuman = getFormListFromIndexes(cleaned);
+	var cleanedSorted = sortLiteralsWithinSets(cleaned);
+	var simplifiedCleanedSorted = getSymmetricalDifferences(cleanedSorted);
+	var simplifiedCleanedSortedNonRep = filterOutRepeatingLiteralsLists(simplifiedCleanedSorted);
+	var bhi = generateBaseHypotheses(simplifiedCleanedSortedNonRep);
+	var bhiHuman = getFormListFromIndexes(bhi);
+	var bhi_sorted = sortLiteralsWithinSets(bhi);
+	var bhi_cons = filterOutNonConsistentLiteralsLists(bhi_sorted);
+	var bhi_consHuman = getFormListFromIndexes(bhi_cons);
+	var bhi_non_rep = filterOutRepeatingLiteralsLists(bhi_cons);
+	var bhi_non_repHuman = getFormListFromIndexes(bhi_non_rep);
+	var simplified = getSymmetricalDifferences(bhi_non_rep);
+	var simpl_non_rep = filterOutRepeatingLiteralsLists(simplified);
+	var simpl_non_repHuman = getFormListFromIndexes(simpl_non_rep);
+	var minimalSet = removeLiteralsSupSets(simpl_non_rep);
+	var minimalSetHuman = getFormListFromIndexes(minimalSet);
+	 
+	var baseHypotheses  = Vector.new();
+	var i;
+	for(i = 0; i < minimalSet.size; i++)
+		baseHypotheses.add(formulaFromLiterals(minimalSet[i])); 
+		
+	//Functions converting	encoded literals into human readable formats
+	var hypothesesAllBinary = generateBinaryCombinations(baseHypotheses.size);
+	var setLatex = convertIndexedSetToLatex(set);
+	var dnf = binaryToForm(hypothesesAllBinary[hypothesesAllBinary.size - 1], baseHypotheses);
+	var infix = Vector.new(); 
+	infix = indexesPrefixToInfix(form, infix);
+	var formInfix = createInfixFormFromIndexesInfix(infix);
+	var formLatex = formToLatex(formInfix);
+		
+	//Printing out the most important information into the specified earlier output file 	
+	writeInfo(file_name, "#set: " + setLatex + "\n#form: " + formLatex  + "\n");
+	writeInfo(file_name, "#tableau-validation: " + valid + "\n");
+	writeInfo(file_name, "#\n");	
+	writeInfo(file_name, "#base hypotheses count:\n");
+	writeInfo(file_name, "#raw-size: " + entangledLiterals.size + "\n");
+	writeInfo(file_name, "#cleaned-size: " + cleaned.size + "\n");
+	writeInfo(file_name, "#non-filtered-raw: nf=" + entangledLiterals[0].size);
+	
+	for(i = 1; i <  entangledLiterals.size; i++)
+		writeInfo(file_name,"*" + entangledLiterals[i].size);
+		
+	writeInfo(file_name, "\n#entangled-literals-raw: NA \n");
+	writeInfo(file_name, "#non-filtered: nf=" + cleaned[0].size);
+		
+	for(i = 1; i <  cleaned.size; i++)
+		writeInfo(file_name,"*" + cleaned[i].size);
+		
+	writeInfo(file_name, "\n");
+	writeInfo(file_name, "#entangled-literals: " + cleanedHuman + "\n");
+	writeInfo(file_name, "#simplify-stage-1-size: " + bhi.size + "\n");
+	writeInfo(file_name, "#simplify-stage-1-hypotheses: " + bhiHuman + "\n");
+	writeInfo(file_name, "#simplify-stage-1-consistent-size: " + bhi_cons.size + "\n");
+	writeInfo(file_name, "#simplify-stage-1-consistent-hypotheses: " + bhi_consHuman + "\n");
+	writeInfo(file_name, "#simplify-stage-1-consistent-non_repeated-size: " + bhi_non_rep.size + "\n");
+	writeInfo(file_name, "#simplify-stage-1-consistent-non_repeated-hypotheses: " + bhi_non_repHuman + "\n");
+	writeInfo(file_name, "#simplify-stage-2-size: " + simpl_non_rep.size + "\n");
+	writeInfo(file_name, "#simplify-stage-2-hypotheses: " + simpl_non_repHuman + "\n");
+	writeInfo(file_name, "#simplify-stage-3-size: " + minimalSet.size + "\n");
+	writeInfo(file_name, "#simplify-stage-3-hypotheses: " + minimalSetHuman + "\n");
+	writeInfo(file_name, "#number	formatChar	prefix_form	infix_form	formatHumanLatex_infix\n");
+	
+	
+	//Generation and printing out of the base abductive hypotheses
+	for(i = 0; i < hypothesesAllBinary.size; i++)
+	{
+		var current = binaryToForm(hypothesesAllBinary[i], baseHypotheses);
+		var currentIndexed = binaryToIndex(hypothesesAllBinary[i], minimalSet);		
+		writeInfo(file_name,"" + (i+1) + "	" + hypothesesAllBinary[i] + "	" + current + "	");
+		
+		var infix = Vector.new();
+		infix = indexesPrefixToInfix(currentIndexed, infix);
+		var formInfix = createInfixFormFromIndexesInfix(infix);
+		var latex = formToLatex(formInfix);
+		writeInfo(file_name,""  + formInfix + "	" + latex + "\n");
+	}
+	
+}
+
+@include "abduction_misc.inc"
+@include "data_conversion.inc"
+@include "formulas_processing.inc"
+@include "lists_processing.inc"
+@include "literals_processing.inc"
+@include "synthetic_rules.inc"
+@include "synthetic_tableau.inc"
+
+~
+
+prop:
+id:params
+name:Logical experiment parameters
+help:See readme-abduction.txt
+type:s
+
Index: experiments/frams/logic/data/scripts/synthetic_rules.inc
===================================================================
--- experiments/frams/logic/data/scripts/synthetic_rules.inc	(revision 169)
+++ experiments/frams/logic/data/scripts/synthetic_rules.inc	(revision 169)
@@ -0,0 +1,224 @@
+//This file contains functions synthesizing logical formulas and enabling transmission of entangled literals
+
+function syntheticImplNARule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	
+	if(firstArg[0][0] == 0)
+	{	
+		result.add([3]);
+		var i;
+		
+		for(i = 1; i < firstArg[0].size; i++)
+			result[0].add(firstArg[0][i]);
+			
+		for(i = 0; i < secondArg[0].size; i++)	
+			result[0].add(secondArg[0][i]);
+					
+		result.add(deepCopyList(firstArg[1]));
+		
+	}	
+	
+	return result;
+}
+
+function syntheticImplBRule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	result.add([3]);
+	
+	var i;
+		
+	for(i = 0; i < firstArg[0].size; i++)
+		result[0].add(firstArg[0][i]);
+			
+	for(i = 0; i < secondArg[0].size; i++)	
+		result[0].add(secondArg[0][i]);
+					
+	result.add(deepCopyList(secondArg[1]));
+		
+	return result;
+}
+
+function syntheticImplANBRule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	
+	if(secondArg[0][0] == 0)
+	{
+		result.add([0,3]);
+		var i;
+		
+		for(i = 0; i < firstArg[0].size; i++)
+			result[0].add(firstArg[0][i]);
+			
+		for(i = 1; i < secondArg[0].size; i++)	
+			result[0].add(secondArg[0][i]);
+		
+		result.add(deepCopyList(firstArg[1]));
+		
+		for(i = 0; i < secondArg[1].size; i++)
+		{
+			//do not let an entangled literal to be repeated
+			if(result[1].find(secondArg[1][i]) == -1)
+				result[1].add(deepCopyList(secondArg[1][i]));
+		}
+	}
+	
+	return result;
+}
+
+function syntheticAltARule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	result.add([2]);
+	
+	var i;
+	
+	for(i = 0; i < firstArg[0].size; i++)
+		result[0].add(firstArg[0][i]);
+			
+	for(i = 0; i < secondArg[0].size; i++)	
+		result[0].add(secondArg[0][i]);
+	
+	result.add(deepCopyList(firstArg[1]));	
+		
+	return result;
+}
+
+function syntheticAltBRule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	
+	result.add([2]);
+	
+	var i;
+	
+	for(i = 0; i < firstArg[0].size; i++)
+		result[0].add(firstArg[0][i]);
+			
+	for(i = 0; i < secondArg[0].size; i++)	
+		result[0].add(secondArg[0][i]);
+	
+	result.add(deepCopyList(secondArg[1]));	
+		
+	return result;
+}
+
+
+function syntheticAltNANBRule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	
+	if(firstArg[0][0] == 0 && secondArg[0][0] == 0)
+	{	
+		
+		result.add([0,2]);
+		
+		var i;
+	
+		for(i = 1; i < firstArg[0].size; i++)
+			result[0].add(firstArg[0][i]);
+			
+		for(i = 1; i < secondArg[0].size; i++)	
+			result[0].add(secondArg[0][i]);
+		
+		
+		result.add(deepCopyList(firstArg[1]));
+		
+		for(i = 0; i < secondArg[1].size; i++)
+		{
+			//do not let an entangled literal to be repeated
+			if(result[1].find(secondArg[1][i]) == -1)
+				result[1].add(deepCopyList(secondArg[1][i]));
+		}
+		
+	}	
+	return result;
+}
+
+function syntheticConjNARule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	
+	
+	if(firstArg[0][0] == 0)
+	{
+		result.add([0,1]);
+		var i;
+		
+		
+		for(i = 1; i < firstArg[0].size; i++)
+			result[0].add(firstArg[0][i]);
+			
+		for(i = 0; i < secondArg[0].size; i++)	
+			result[0].add(secondArg[0][i]);
+		
+		
+		result.add(deepCopyList(firstArg[1]));
+			
+	}	
+	return result;
+}
+
+function syntheticConjNBRule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	
+	if(secondArg[0][0] == 0)
+	{
+		result.add([0,1]);
+		var i;
+		
+		for(i = 0; i < firstArg[0].size; i++)
+			result[0].add(firstArg[0][i]);
+			
+		for(i = 1; i < secondArg[0].size; i++)	
+			result[0].add(secondArg[0][i]);
+		
+		result.add(deepCopyList(secondArg[1]));			
+		
+	}	
+	return result;
+}
+
+function syntheticConjABRule(firstArg, secondArg)
+{
+	var result = Vector.new();
+	result.add([1]);
+	
+	var i;
+	
+	for(i = 0; i < firstArg[0].size; i++)
+		result[0].add(firstArg[0][i]);
+			
+	for(i = 0; i < secondArg[0].size; i++)	
+		result[0].add(secondArg[0][i]);
+	
+	
+	result.add(deepCopyList(secondArg[1]));
+	
+	for(i = 0; i < secondArg[1].size; i++)
+	{
+		//do not let an entangled literal to be repeated
+		if(result[1].find(secondArg[1][i]) == -1)
+			result[1].add(deepCopyList(secondArg[1][i]));
+	}
+				
+	return result;
+}
+
+function syntheticNegRule(arg)
+{
+	var result = Vector.new();
+	result.add([0,0]);
+	
+	var i;
+	
+	for(i = 0; i < arg[0].size; i++)
+		result[0].add(arg[0][i]);
+	
+	result.add(deepCopyList(arg[1]));
+	
+	return result;
+}
Index: experiments/frams/logic/data/scripts/synthetic_tableau.inc
===================================================================
--- experiments/frams/logic/data/scripts/synthetic_tableau.inc	(revision 169)
+++ experiments/frams/logic/data/scripts/synthetic_tableau.inc	(revision 169)
@@ -0,0 +1,327 @@
+//This file contains synthetic tableau generation functions and support methods.
+
+function generateSyntheticInfFromSetIndexed(formulasIndexed, subformulasIndexed, variablesIndexed)
+{
+	var i,j;
+	
+	var tableau = generateSyntheticTableauIndexed(formulasIndexed, subformulasIndexed, variablesIndexed);
+	
+	var inferences = Vector.new();
+	getSyntheticInferences(tableau, inferences);
+	
+	return inferences;
+}
+
+function generateSyntheticTableauIndexed(formulasIndexed, subformulasIndexed, variablesIndexed)
+{
+	var i;
+	var stack = Vector.new();
+	var tableau = Vector.new();
+	var stop = 0;
+	var result = Vector.new();
+	
+		tableau.add([1]);
+		tableau.add([1]);
+		
+		
+		stack.add(tableau[0]);
+		stack.add(tableau[1]);
+		
+		var branching = createSyntheticBranchingIndexed(variablesIndexed[0]);
+		tableau.get(tableau.size - 2).add(branching[0]);
+		tableau.get(tableau.size - 1).add(branching[1]);
+		
+		result.add(tableau[0]);
+		result.add(tableau[1]);
+	
+		tableau = stack[0];
+		
+	while(stack.size > 0)
+	{
+		applyRulesToInferenceIndexed(tableau, subformulasIndexed);
+		stop = searchFormsThroughInference(formulasIndexed, tableau);
+		stack.remove(0);
+		
+		if(stop == 1)
+		{		
+			if(stack.size > 0)
+			{
+				tableau = stack[0];
+				continue;
+			}	
+		}	
+		if(variablesIndexed.size > tableau[0])
+		{	
+			var branching = createSyntheticBranchingIndexed(variablesIndexed[tableau[0]]);
+			
+			tableau.add([tableau[0] + 1]);
+			tableau.add([tableau[0] + 1]);
+			
+			for(i = 1; i < tableau.size - 2; i++)
+			{	
+				tableau[tableau.size - 1].add(tableau[i]);
+				tableau[tableau.size - 2].add(tableau[i]);
+			}
+			
+			tableau[tableau.size - 1].add(branching[0]);
+			tableau[tableau.size - 2].add(branching[1]);
+			
+			stack.add(tableau[tableau.size - 2]);
+			stack.add(tableau[tableau.size - 1]);
+			
+			var tableau_size_temp = tableau.size - 2; 
+		
+			for(i = 0; i < tableau_size_temp; i++)
+			{
+				tableau.remove(0);
+			}
+			tableau = stack[0];	
+		}
+	}	
+	return result;
+}
+
+
+
+function createSyntheticBranchingIndexed(variableIndexed)
+{	
+	var branching = Vector.new();
+	
+	branching.add([[variableIndexed[0]],[[variableIndexed[0]]]]);
+	branching.add([[0,variableIndexed[0]], [[0, variableIndexed[0]]]]);
+	
+	return branching;
+}
+
+function applyRulesToInferenceIndexed(inferenceIndexed, subformulasIndexed)
+{
+	var i,j;
+	var check = 1;
+	var tempForms = Vector.new();
+	var merged = Vector.new();
+		
+	while(check == 1)
+	{
+		check = 0;
+		merged = mergeInferencesSubformulasIndexed(inferenceIndexed, subformulasIndexed);
+		//TODO modernizne temp
+		for(i = 1; i < inferenceIndexed.size; i++)
+		{
+			for(j = 1; j < inferenceIndexed.size; j++)
+			{
+					tempForms.add(syntheticNegRule(inferenceIndexed[i]));
+					tempForms.add(syntheticImplANBRule(inferenceIndexed[i], inferenceIndexed[j]));
+					tempForms.add(syntheticAltNANBRule(inferenceIndexed[i], inferenceIndexed[j]));
+					tempForms.add(syntheticConjABRule(inferenceIndexed[i], inferenceIndexed[j]));	
+			}
+				
+			for(j = 1; j < merged.size; j++)
+			{
+				tempForms.add(syntheticImplNARule(inferenceIndexed[i], merged[j]));
+				tempForms.add(syntheticImplBRule(merged[j], inferenceIndexed[i]));
+				tempForms.add(syntheticAltARule(inferenceIndexed[i], merged[j]));
+				tempForms.add(syntheticAltBRule(merged[j], inferenceIndexed[i]));
+				tempForms.add(syntheticConjNARule(inferenceIndexed[i], merged[j]));
+				tempForms.add(syntheticConjNBRule(merged[j], inferenceIndexed[i]));
+			}
+		}
+		for(i = 0; i < tempForms.size; i++)
+		{
+			if(validateSynthesizedFormulaIndexed(tempForms[i], subformulasIndexed) == 1)
+			{
+				for(j = 1; j < inferenceIndexed.size; j++)
+					if(verifyPlainListsIdentity(tempForms[i][0], inferenceIndexed[j][0]) == 1)
+						continue 2;
+							
+				inferenceIndexed.add(tempForms[i]);
+				check = 1;
+			}
+			
+		}
+		
+		merged.clear();
+		tempForms.clear();
+	}
+}
+function searchFormsThroughInference(formulasIndexed, inferenceIndexed)
+{
+	var i,j;
+	var stop = 0;
+	var negFormIndexed = Vector.new();
+	
+	for(i = 0; i < formulasIndexed.size; i++)
+	{
+		
+		for(j = 1; j < inferenceIndexed.size; j++)
+		{
+			negFormIndexed = plainListCopyInsert(formulasIndexed[i], 0, [0]);
+			if(verifyPlainListsIdentity(formulasIndexed[i], inferenceIndexed[j][0]) == 1 || verifyPlainListsIdentity(negFormIndexed, inferenceIndexed[j][0]) == 1)
+			{
+				stop = 1;
+				continue 2;
+			}
+		}
+		return 0;
+	}
+	
+	return stop;
+}
+
+function mergeInferencesSubformulasIndexed(inferenceIndexed, subformulasIndexed)
+{
+	var result = Vector.new();
+	var i,j;
+		
+	for(i = 0; i < inferenceIndexed.size; i++)
+	{
+		result.add(inferenceIndexed[i]);
+	}
+		
+	for(i = 0; i < subformulasIndexed.size; i++)
+	{
+		for(j = 1; j < inferenceIndexed.size; j++)
+		{
+			if(subformulasIndexed[i] == inferenceIndexed[j][0])
+			{
+				continue 2;
+			}
+		}
+		
+		result.add(Vector.new());
+		result.get(result.size - 1).add(subformulasIndexed[i]);					
+	}
+	
+	return result;
+	
+}
+
+
+function validateSynthesizedFormulaIndexed(formulaIndexed, subformulasIndexed)
+{
+	if(formulaIndexed.size < 2)
+		return 0;
+		
+	if(findPlainList(subformulasIndexed, formulaIndexed[0]) != -1)
+	{
+		return 1;
+	}
+	else
+	{
+		
+		if(formulaIndexed[0][0] == 0)
+		{
+			var tempFormula = plainListRight(formulaIndexed[0], formulaIndexed[0].size - 1);
+			if(findPlainList(subformulasIndexed, tempFormula) != -1)
+				return 1;
+		}
+	}
+	return 0;
+	
+}
+
+function getSyntheticInferences(tableau, inferences)
+{
+	
+	if(typeof(tableau.get(0)) == "Vector")
+	{
+		var i;
+		
+		for(i = 0; i < tableau.size; i++)
+			getSyntheticInferences(tableau.get(i), inferences);
+			
+		return inferences;
+	}
+	else
+	{
+		inferences.add(tableau);
+		return inferences;
+	}
+}
+
+
+
+function getFailures(inferencesIndexed, formulasIndexed)
+{
+	var partialTableau = Vector.new();
+	var branchesNum = Vector.new();
+	var i;
+	
+	for(i = 0; i < inferencesIndexed.size; i++)
+	{
+		if(syntheticInferenceFailure(inferencesIndexed[i], formulasIndexed) == 1)
+		{
+			partialTableau.add(inferencesIndexed[i]);
+			branchesNum.add(i);
+		}
+	}		
+	return [partialTableau,branchesNum];
+}
+
+
+function syntheticInferenceFailure(inferenceIndexed, formulasIndexed)
+{
+	var i,j;
+	
+	for(i = 1; i < inferenceIndexed.size; i++)
+		if(verifyPlainListsIdentity(formulasIndexed[formulasIndexed.size - 1], inferenceIndexed[i][0]))
+			return 0;
+	
+	var negFormulaIndexed = Vector.new();	
+	for(i = 0; i < formulasIndexed.size - 1; i++)
+		for(j = 1; j < inferenceIndexed.size; j++)
+		{
+			negFormulaIndexed = plainListCopyInsert(formulasIndexed[i], 0, [0]);
+			if(verifyPlainListsIdentity(negFormulaIndexed, inferenceIndexed[j][0]))
+				return 0;
+		}	
+		
+	return 1;
+}
+
+function checkTableauSuccess(inferences, formulas)
+{
+	var i;
+	for(i = 0; i < inferences.size; i++)
+	{
+		if(syntheticInferenceFailure(inferences.get(i), formulas) == 1)
+		{
+				return 0;
+		}
+	}
+		
+	return 1;
+}
+
+function checkTableValidity(inferences, formulas)
+{
+	var i;
+	for(i = 0;  i < inferences.size; i++)
+		{
+			if(checkSyntheticInferenceValidity(inferences[i], formulas) == 0)
+			{
+				return 0;
+			}
+		}
+		
+	return 1;
+} 
+
+function checkSyntheticInferenceValidity(inference, formulas)
+{
+	var i,j;
+	
+	for(i = 0; i < formulas.size; i++)
+	{
+		for(j = 1; j < inference.size; j++)
+		{
+			if((verifyPlainListsIdentity(plainListCopyInsert(formulas[i],0,[0]), inference[j][0]) == 1)||( verifyPlainListsIdentity(formulas[i], inference[j][0]) == 1))
+			{
+				continue 2;
+				
+			}
+		}	
+		return 0;
+	}
+	
+	return 1;
+}
Index: experiments/frams/logic/readme-abduction.txt
===================================================================
--- experiments/frams/logic/readme-abduction.txt	(revision 169)
+++ experiments/frams/logic/readme-abduction.txt	(revision 169)
@@ -0,0 +1,34 @@
+The run-abduction.cmd script demonstrates how to use logical abduction experiment definition. 
+Experiment parameters are passed as string sequences separated by semicolons.
+
+Note that logical formulas have to be entered using the prefix format. Symbols
+forming a formula have to be separated by an underscore. 
+
+The logical symbols are:
+
+conjuction:
+N - negation 
+K - conjunction
+A - alternative
+C - consequence
+
+propositional variables available:
+p,q,r,s,t,u,v,w,x 
+
+An example:
+A formula '(p or q) => r' in the infix format should be encoded as 'C_A_p_q_r'. 
+
+The first parameter is the abductive goal. Next, there is a list of logical formulas 
+separated by whitespaces constituting a database. The last parameter is the output
+file name. The output file name will be suffixed with 'RawHyp', and the file
+will be placed in the '/data/scripts_output/' directory. The file will contain
+a lot of information about the problem and the obtained abductive hypotheses.
+
+Note:
+The experiment definition is currently under developement. One of the
+issues which are yet to be solved is the low capacity of the program to solve 
+problems which contain many distinct variables (but not occurences of these variables). 
+Currently, the script is able to compute in a reasonable time problems
+containg up to four distinct variables. Problems containg more variables may
+take several hours to compute.
+
Index: experiments/frams/logic/run-abduction.cmd
===================================================================
--- experiments/frams/logic/run-abduction.cmd	(revision 169)
+++ experiments/frams/logic/run-abduction.cmd	(revision 169)
@@ -0,0 +1,13 @@
+rem See readme-abduction.txt!
+
+rem The two calls below launch "frams", which is a command-line interface (CLI) of Framsticks.
+rem You can also launch the Framsticks GUI, select the "abduction" experiment definition, set params, initialize experiment and run it.
+
+
+
+rem The abduction problem consting of an abductive goal being a simple conjuction and two formulas forming a database:
+frams "ex logic_abduction" "ExpParams.params=\"K_q_s;C_p_q C_r_s;abdOut1.txt\"; Simulator.init();" "go" "qu"
+
+rem The abduction problem consting of an abductive goal being a propositional variable and two formulas forming a database:
+frams "ex logic_abduction" "ExpParams.params=\"q;C_K_p_r_q C_C_N_r_q_p;abdOut2.txt\"; Simulator.init();" "go" "qu"
+
