source: experiments/frams/logic/data/scripts/synthetic_tableau.inc @ 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: 7.2 KB
Line 
1//This file contains synthetic tableau generation functions and support methods.
2
3function generateSyntheticInfFromSetIndexed(formulasIndexed, subformulasIndexed, variablesIndexed)
4{
5        var i,j;
6       
7        var tableau = generateSyntheticTableauIndexed(formulasIndexed, subformulasIndexed, variablesIndexed);
8       
9        var inferences = Vector.new();
10        getSyntheticInferences(tableau, inferences);
11       
12        return inferences;
13}
14
15function generateSyntheticTableauIndexed(formulasIndexed, subformulasIndexed, variablesIndexed)
16{
17        var i;
18        var stack = Vector.new();
19        var tableau = Vector.new();
20        var stop = 0;
21        var result = Vector.new();
22       
23                tableau.add([1]);
24                tableau.add([1]);
25               
26               
27                stack.add(tableau[0]);
28                stack.add(tableau[1]);
29               
30                var branching = createSyntheticBranchingIndexed(variablesIndexed[0]);
31                tableau.get(tableau.size - 2).add(branching[0]);
32                tableau.get(tableau.size - 1).add(branching[1]);
33               
34                result.add(tableau[0]);
35                result.add(tableau[1]);
36       
37                tableau = stack[0];
38               
39        while(stack.size > 0)
40        {
41                applyRulesToInferenceIndexed(tableau, subformulasIndexed);
42                stop = searchFormsThroughInference(formulasIndexed, tableau);
43                stack.remove(0);
44               
45                if(stop == 1)
46                {               
47                        if(stack.size > 0)
48                        {
49                                tableau = stack[0];
50                                continue;
51                        }       
52                }       
53                if(variablesIndexed.size > tableau[0])
54                {       
55                        var branching = createSyntheticBranchingIndexed(variablesIndexed[tableau[0]]);
56                       
57                        tableau.add([tableau[0] + 1]);
58                        tableau.add([tableau[0] + 1]);
59                       
60                        for(i = 1; i < tableau.size - 2; i++)
61                        {       
62                                tableau[tableau.size - 1].add(tableau[i]);
63                                tableau[tableau.size - 2].add(tableau[i]);
64                        }
65                       
66                        tableau[tableau.size - 1].add(branching[0]);
67                        tableau[tableau.size - 2].add(branching[1]);
68                       
69                        stack.add(tableau[tableau.size - 2]);
70                        stack.add(tableau[tableau.size - 1]);
71                       
72                        var tableau_size_temp = tableau.size - 2;
73               
74                        for(i = 0; i < tableau_size_temp; i++)
75                        {
76                                tableau.remove(0);
77                        }
78                        tableau = stack[0];     
79                }
80        }       
81        return result;
82}
83
84
85
86function createSyntheticBranchingIndexed(variableIndexed)
87{       
88        var branching = Vector.new();
89       
90        branching.add([[variableIndexed[0]],[[variableIndexed[0]]]]);
91        branching.add([[0,variableIndexed[0]], [[0, variableIndexed[0]]]]);
92       
93        return branching;
94}
95
96function applyRulesToInferenceIndexed(inferenceIndexed, subformulasIndexed)
97{
98        var i,j;
99        var check = 1;
100        var tempForms = Vector.new();
101        var merged = Vector.new();
102               
103        while(check == 1)
104        {
105                check = 0;
106                merged = mergeInferencesSubformulasIndexed(inferenceIndexed, subformulasIndexed);
107                //TODO modernizne temp
108                for(i = 1; i < inferenceIndexed.size; i++)
109                {
110                        for(j = 1; j < inferenceIndexed.size; j++)
111                        {
112                                        tempForms.add(syntheticNegRule(inferenceIndexed[i]));
113                                        tempForms.add(syntheticImplANBRule(inferenceIndexed[i], inferenceIndexed[j]));
114                                        tempForms.add(syntheticAltNANBRule(inferenceIndexed[i], inferenceIndexed[j]));
115                                        tempForms.add(syntheticConjABRule(inferenceIndexed[i], inferenceIndexed[j]));   
116                        }
117                               
118                        for(j = 1; j < merged.size; j++)
119                        {
120                                tempForms.add(syntheticImplNARule(inferenceIndexed[i], merged[j]));
121                                tempForms.add(syntheticImplBRule(merged[j], inferenceIndexed[i]));
122                                tempForms.add(syntheticAltARule(inferenceIndexed[i], merged[j]));
123                                tempForms.add(syntheticAltBRule(merged[j], inferenceIndexed[i]));
124                                tempForms.add(syntheticConjNARule(inferenceIndexed[i], merged[j]));
125                                tempForms.add(syntheticConjNBRule(merged[j], inferenceIndexed[i]));
126                        }
127                }
128                for(i = 0; i < tempForms.size; i++)
129                {
130                        if(validateSynthesizedFormulaIndexed(tempForms[i], subformulasIndexed) == 1)
131                        {
132                                for(j = 1; j < inferenceIndexed.size; j++)
133                                        if(verifyPlainListsIdentity(tempForms[i][0], inferenceIndexed[j][0]) == 1)
134                                                continue 2;
135                                                       
136                                inferenceIndexed.add(tempForms[i]);
137                                check = 1;
138                        }
139                       
140                }
141               
142                merged.clear();
143                tempForms.clear();
144        }
145}
146function searchFormsThroughInference(formulasIndexed, inferenceIndexed)
147{
148        var i,j;
149        var stop = 0;
150        var negFormIndexed = Vector.new();
151       
152        for(i = 0; i < formulasIndexed.size; i++)
153        {
154               
155                for(j = 1; j < inferenceIndexed.size; j++)
156                {
157                        negFormIndexed = plainListCopyInsert(formulasIndexed[i], 0, [0]);
158                        if(verifyPlainListsIdentity(formulasIndexed[i], inferenceIndexed[j][0]) == 1 || verifyPlainListsIdentity(negFormIndexed, inferenceIndexed[j][0]) == 1)
159                        {
160                                stop = 1;
161                                continue 2;
162                        }
163                }
164                return 0;
165        }
166       
167        return stop;
168}
169
170function mergeInferencesSubformulasIndexed(inferenceIndexed, subformulasIndexed)
171{
172        var result = Vector.new();
173        var i,j;
174               
175        for(i = 0; i < inferenceIndexed.size; i++)
176        {
177                result.add(inferenceIndexed[i]);
178        }
179               
180        for(i = 0; i < subformulasIndexed.size; i++)
181        {
182                for(j = 1; j < inferenceIndexed.size; j++)
183                {
184                        if(subformulasIndexed[i] == inferenceIndexed[j][0])
185                        {
186                                continue 2;
187                        }
188                }
189               
190                result.add(Vector.new());
191                result.get(result.size - 1).add(subformulasIndexed[i]);                                 
192        }
193       
194        return result;
195       
196}
197
198
199function validateSynthesizedFormulaIndexed(formulaIndexed, subformulasIndexed)
200{
201        if(formulaIndexed.size < 2)
202                return 0;
203               
204        if(findPlainList(subformulasIndexed, formulaIndexed[0]) != -1)
205        {
206                return 1;
207        }
208        else
209        {
210               
211                if(formulaIndexed[0][0] == 0)
212                {
213                        var tempFormula = plainListRight(formulaIndexed[0], formulaIndexed[0].size - 1);
214                        if(findPlainList(subformulasIndexed, tempFormula) != -1)
215                                return 1;
216                }
217        }
218        return 0;
219       
220}
221
222function getSyntheticInferences(tableau, inferences)
223{
224       
225        if(typeof(tableau.get(0)) == "Vector")
226        {
227                var i;
228               
229                for(i = 0; i < tableau.size; i++)
230                        getSyntheticInferences(tableau.get(i), inferences);
231                       
232                return inferences;
233        }
234        else
235        {
236                inferences.add(tableau);
237                return inferences;
238        }
239}
240
241
242
243function getFailures(inferencesIndexed, formulasIndexed)
244{
245        var partialTableau = Vector.new();
246        var branchesNum = Vector.new();
247        var i;
248       
249        for(i = 0; i < inferencesIndexed.size; i++)
250        {
251                if(syntheticInferenceFailure(inferencesIndexed[i], formulasIndexed) == 1)
252                {
253                        partialTableau.add(inferencesIndexed[i]);
254                        branchesNum.add(i);
255                }
256        }               
257        return [partialTableau,branchesNum];
258}
259
260
261function syntheticInferenceFailure(inferenceIndexed, formulasIndexed)
262{
263        var i,j;
264       
265        for(i = 1; i < inferenceIndexed.size; i++)
266                if(verifyPlainListsIdentity(formulasIndexed[formulasIndexed.size - 1], inferenceIndexed[i][0]))
267                        return 0;
268       
269        var negFormulaIndexed = Vector.new();   
270        for(i = 0; i < formulasIndexed.size - 1; i++)
271                for(j = 1; j < inferenceIndexed.size; j++)
272                {
273                        negFormulaIndexed = plainListCopyInsert(formulasIndexed[i], 0, [0]);
274                        if(verifyPlainListsIdentity(negFormulaIndexed, inferenceIndexed[j][0]))
275                                return 0;
276                }       
277               
278        return 1;
279}
280
281function checkTableauSuccess(inferences, formulas)
282{
283        var i;
284        for(i = 0; i < inferences.size; i++)
285        {
286                if(syntheticInferenceFailure(inferences.get(i), formulas) == 1)
287                {
288                                return 0;
289                }
290        }
291               
292        return 1;
293}
294
295function checkTableValidity(inferences, formulas)
296{
297        var i;
298        for(i = 0;  i < inferences.size; i++)
299                {
300                        if(checkSyntheticInferenceValidity(inferences[i], formulas) == 0)
301                        {
302                                return 0;
303                        }
304                }
305               
306        return 1;
307}
308
309function checkSyntheticInferenceValidity(inference, formulas)
310{
311        var i,j;
312       
313        for(i = 0; i < formulas.size; i++)
314        {
315                for(j = 1; j < inference.size; j++)
316                {
317                        if((verifyPlainListsIdentity(plainListCopyInsert(formulas[i],0,[0]), inference[j][0]) == 1)||( verifyPlainListsIdentity(formulas[i], inference[j][0]) == 1))
318                        {
319                                continue 2;
320                               
321                        }
322                }       
323                return 0;
324        }
325       
326        return 1;
327}
Note: See TracBrowser for help on using the repository browser.