1 | expdef: |
---|
2 | name:Generate abductive hypotheses |
---|
3 | info:~ |
---|
4 | This experiment definition generates abducibles for a specified abductive problem. |
---|
5 | |
---|
6 | Results and details are published in Transactions on Computational Logic, 2014, |
---|
7 | "Identifying efficient abductive hypotheses using multi-criteria dominance relation" |
---|
8 | by M. Komosinski, A. Kups, D. Leszczynska-Jasion and M. Urbanski. |
---|
9 | |
---|
10 | See also readme-abduction.txt and run-abduction.cmd. |
---|
11 | ~ |
---|
12 | code:~ |
---|
13 | |
---|
14 | global g_params; |
---|
15 | global g_form; |
---|
16 | global g_set; |
---|
17 | global g_file; |
---|
18 | global g_symbolsChart; |
---|
19 | global g_oldSymbolsChart; |
---|
20 | |
---|
21 | function 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 | |
---|
42 | function 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 | |
---|
80 | function 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 |
---|
95 | function 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 | |
---|
151 | function 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 | |
---|
254 | prop: |
---|
255 | id:params |
---|
256 | name:Logical experiment parameters |
---|
257 | help:See readme-abduction.txt |
---|
258 | type:s |
---|
259 | |
---|