source: experiments/frams/logic/data/scripts/logic_abduction.expdef @ 1052

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