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

Last change on this file since 169 was 169, checked in by Maciej Komosinski, 10 years ago

A library of logic functions, an experiment definition that generates abductive hypotheses, and a script that runs sample experiments

File size: 8.5 KB
RevLine 
[169]1expdef:
2name:Generate abductive hypotheses
3info:~
4This experiment definition generates abducibles for a specified abductive problem.
5
6Results and details are published in Transactions on Computational Logic, 2014,
7"Identifying efficient abductive hypotheses using multi-criteria dominance relation"
8by M. Komosinski, A. Kups, D. Leszczynska-Jasion and M. Urbanski.
9
10See also readme-abduction.txt and run-abduction.cmd.
11~
12code:~
13
14global g_params;
15global g_form;
16global g_set;
17global g_file;
18global g_symbolsChart;
19global g_oldSymbolsChart;
20
21function onExpDefLoad()
22{
23  GenePools.clear();
24  Populations.clear();
25  Populations[0].clear();
26 
27  Math.randomize();
28       
29       
30        var g_params = Vector.new();
31       
32        //Logical symbols chart including up to nine distinct variables
33        g_symbolsChart = ["N", "K", "A", "C", "p", "q", "r", "s", "t", "u", "v", "w", "x"];
34       
35        g_form = Vector.new();
36        g_set = Vector.new();
37        g_file = "";   
38
39}
40
41
42function onExpInit()
43{
44        //Initialization of the experiment parameters loaded from file
45        g_params = String.split(ExpParams.params, ";");
46        if(g_params.size == 3)
47        {
48                //Conversion of the string characters into a numerical encoding
49                var i,j;
50                var splitedForm = String.split(g_params[0],"_");
51               
52                for(i = 0; i < splitedForm.size; i++)
53                {
54                        g_form.add(g_symbolsChart.find(splitedForm[i]));
55                }
56               
57                var splitedSet = String.split(g_params[1], " ");
58                var splitedElt = Vector.new();
59               
60                for(i = 0; i < splitedSet.size; i++)
61                {
62                        g_set.add(Vector.new());
63                        splitedElt = String.split(splitedSet[i], "_"); 
64               
65                        for(j = 0; j < splitedElt.size; j++)
66                        {
67                                g_set[i].add(g_symbolsChart.find(splitedElt[j]));
68                        }
69                }
70               
71                g_file = g_params[2];
72               
73        } else
74          {
75                Simulator.print("Something is not right with the experiment parameters!");
76          }
77         
78}
79
80function onStep()
81{
82        if(g_params.size == 3)
83        {
84                //Call of the main function of the experiment
85                getRawHypotheses(g_set, g_form, g_file);
86                Simulator.stop();
87        } else
88          {
89                Simulator.print("Something is wrong with experiment parameters! Stopping simulation...");
90                Simulator.stop();
91          }
92}
93
94//Main function of the experiment
95function getRawHypotheses(set, form, fileName)
96{
97                var i,j;
98                //Generation of the list containg all the formulas of the problem
99                var formulas = Vector.new();
100                for(i = 0; i < set.size; i++)
101                        formulas.add(set[i]);
102               
103                formulas.add(form);     
104                //Generation of the list containing all the subformulas of the problem
105                var subformulas = Vector.new();
106                for(i = 0; i < formulas.size; i++)
107                {
108               
109                        var tempSf = getSubFormulasIndexed(formulas[i]);
110                        for(j = 0; j < tempSf.size; j++)
111                        {
112                                if(findPlainList(subformulas, tempSf[j]) == -1)
113                                        subformulas.add(tempSf[j]);
114                        }
115                       
116                }
117       
118                //Generation of the list containing all the variables of the problem
119                var variables = getVariablesIndexed(subformulas);
120               
121                //Generation of the synthetic inferences list
122                var inferences = generateSyntheticInfFromSetIndexed(formulas, subformulas, variables);
123               
124                //Checking whether a tableau is closed
125                var success = checkTableauSuccess(inferences, formulas);
126                if(!success)
127                {
128                        //Generation of the output file name
129                        var fileNSplit = String.split(fileName, ".");
130                        var  fName = fileNSplit[0] + "RawHyp.txt";
131                       
132                        //Generation and preprocessing list of the abductive hypotheses
133                        rawHypothesesGeneration(inferences, set, form, formulas, fName);
134                       
135       
136                } else
137                  {
138                        //Printing out of the output if the table is closed
139                        var setLatex = convertIndexedSetToLatex(set);
140                        var infix = Vector.new();
141                        infix = indexesPrefixToInfix(form, infix);
142                        var formInfix = createInfixFormFromIndexesInfix(infix);
143                        var formLatex = formToLatex(formInfix);
144                       
145                        writeInfo(fileName, "#set: " + setLatex + "     form: " + formLatex + "\n");
146                        writeInfo(fileName, "success\n");
147                  }
148                 
149}
150
151function rawHypothesesGeneration(inferences, set, form, formulas, file_name)
152{
153       
154        var valid = checkTableValidity(inferences, formulas);
155       
156        //Function that gets failure inferences
157        var partialTableaux = getFailures(inferences, formulas);
158        var partialTableau = partialTableaux[0];
159       
160        //Functions that get and reduce entangled literals clauses
161        var entangledLiterals = getEntangledLiterals(partialTableau, formulas);
162        var entangledHuman = getFormListFromIndexes(entangledLiterals);
163        var cleaned = cleanEntangledLiterals(entangledLiterals);
164        var cleanedHuman = getFormListFromIndexes(cleaned);
165        var cleanedSorted = sortLiteralsWithinSets(cleaned);
166        var simplifiedCleanedSorted = getSymmetricalDifferences(cleanedSorted);
167        var simplifiedCleanedSortedNonRep = filterOutRepeatingLiteralsLists(simplifiedCleanedSorted);
168        var bhi = generateBaseHypotheses(simplifiedCleanedSortedNonRep);
169        var bhiHuman = getFormListFromIndexes(bhi);
170        var bhi_sorted = sortLiteralsWithinSets(bhi);
171        var bhi_cons = filterOutNonConsistentLiteralsLists(bhi_sorted);
172        var bhi_consHuman = getFormListFromIndexes(bhi_cons);
173        var bhi_non_rep = filterOutRepeatingLiteralsLists(bhi_cons);
174        var bhi_non_repHuman = getFormListFromIndexes(bhi_non_rep);
175        var simplified = getSymmetricalDifferences(bhi_non_rep);
176        var simpl_non_rep = filterOutRepeatingLiteralsLists(simplified);
177        var simpl_non_repHuman = getFormListFromIndexes(simpl_non_rep);
178        var minimalSet = removeLiteralsSupSets(simpl_non_rep);
179        var minimalSetHuman = getFormListFromIndexes(minimalSet);
180         
181        var baseHypotheses  = Vector.new();
182        var i;
183        for(i = 0; i < minimalSet.size; i++)
184                baseHypotheses.add(formulaFromLiterals(minimalSet[i]));
185               
186        //Functions converting  encoded literals into human readable formats
187        var hypothesesAllBinary = generateBinaryCombinations(baseHypotheses.size);
188        var setLatex = convertIndexedSetToLatex(set);
189        var dnf = binaryToForm(hypothesesAllBinary[hypothesesAllBinary.size - 1], baseHypotheses);
190        var infix = Vector.new();
191        infix = indexesPrefixToInfix(form, infix);
192        var formInfix = createInfixFormFromIndexesInfix(infix);
193        var formLatex = formToLatex(formInfix);
194               
195        //Printing out the most important information into the specified earlier output file   
196        writeInfo(file_name, "#set: " + setLatex + "\n#form: " + formLatex  + "\n");
197        writeInfo(file_name, "#tableau-validation: " + valid + "\n");
198        writeInfo(file_name, "#\n");   
199        writeInfo(file_name, "#base hypotheses count:\n");
200        writeInfo(file_name, "#raw-size: " + entangledLiterals.size + "\n");
201        writeInfo(file_name, "#cleaned-size: " + cleaned.size + "\n");
202        writeInfo(file_name, "#non-filtered-raw: nf=" + entangledLiterals[0].size);
203       
204        for(i = 1; i <  entangledLiterals.size; i++)
205                writeInfo(file_name,"*" + entangledLiterals[i].size);
206               
207        writeInfo(file_name, "\n#entangled-literals-raw: NA \n");
208        writeInfo(file_name, "#non-filtered: nf=" + cleaned[0].size);
209               
210        for(i = 1; i <  cleaned.size; i++)
211                writeInfo(file_name,"*" + cleaned[i].size);
212               
213        writeInfo(file_name, "\n");
214        writeInfo(file_name, "#entangled-literals: " + cleanedHuman + "\n");
215        writeInfo(file_name, "#simplify-stage-1-size: " + bhi.size + "\n");
216        writeInfo(file_name, "#simplify-stage-1-hypotheses: " + bhiHuman + "\n");
217        writeInfo(file_name, "#simplify-stage-1-consistent-size: " + bhi_cons.size + "\n");
218        writeInfo(file_name, "#simplify-stage-1-consistent-hypotheses: " + bhi_consHuman + "\n");
219        writeInfo(file_name, "#simplify-stage-1-consistent-non_repeated-size: " + bhi_non_rep.size + "\n");
220        writeInfo(file_name, "#simplify-stage-1-consistent-non_repeated-hypotheses: " + bhi_non_repHuman + "\n");
221        writeInfo(file_name, "#simplify-stage-2-size: " + simpl_non_rep.size + "\n");
222        writeInfo(file_name, "#simplify-stage-2-hypotheses: " + simpl_non_repHuman + "\n");
223        writeInfo(file_name, "#simplify-stage-3-size: " + minimalSet.size + "\n");
224        writeInfo(file_name, "#simplify-stage-3-hypotheses: " + minimalSetHuman + "\n");
225        writeInfo(file_name, "#number   formatChar      prefix_form     infix_form      formatHumanLatex_infix\n");
226       
227       
228        //Generation and printing out of the base abductive hypotheses
229        for(i = 0; i < hypothesesAllBinary.size; i++)
230        {
231                var current = binaryToForm(hypothesesAllBinary[i], baseHypotheses);
232                var currentIndexed = binaryToIndex(hypothesesAllBinary[i], minimalSet);         
233                writeInfo(file_name,"" + (i+1) + "      " + hypothesesAllBinary[i] + "  " + current + " ");
234               
235                var infix = Vector.new();
236                infix = indexesPrefixToInfix(currentIndexed, infix);
237                var formInfix = createInfixFormFromIndexesInfix(infix);
238                var latex = formToLatex(formInfix);
239                writeInfo(file_name,""  + formInfix + " " + latex + "\n");
240        }
241       
242}
243
244@include "abduction_misc.inc"
245@include "data_conversion.inc"
246@include "formulas_processing.inc"
247@include "lists_processing.inc"
248@include "literals_processing.inc"
249@include "synthetic_rules.inc"
250@include "synthetic_tableau.inc"
251
252~
253
254prop:
255id:params
256name:Logical experiment parameters
257help:See readme-abduction.txt
258type:s
259
Note: See TracBrowser for help on using the repository browser.