Multi-criteria evaluation of abductive hypotheses: towards efficient optimization in proof theory

Research described in this paper aims at implementation of an abductive procedure based on the Synthetic Tableaux Method. This problem concerns a two-stage process of generation and evaluation of abductive hypotheses. While generation of the abductive hypotheses is achieved here by the implementation of the rules provided with a logical apparatus, their evaluation is performed using traditional measures and optimization techniques such as Pareto optimality and fitness–distance analysis. By combining tools known in proof theory and in Artificial Intelligence, we explore the intriguing problem of interpretative reasoning.