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(ExpProperties.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" ~ property: id:params name:Logical experiment parameters help:See readme-abduction.txt type:s