Elena Smirnova

PhD. Thesis

Development and implementation of algorithms for data processing in multivalued logics

Scientific advisers: Pr. Danièle Beauquier, Pr. Nicolai Kossovski


This thesis presents an automated sequent derivation system for multi-valued logics. As an example of multi-valued logic, an extension of Post's Logic with linear order is considered and described in chapter 1. The basic ideas and main algorithms used in this system are presented in this chapter. One of the important parts of the derivation algorithm is a method designed to recognize axioms of a given logic. This method, described in a chapter 2, uses a symbolic computation method for establishing the solvability of systems of linear inequalities of a special type. It is proved that this algorithm has cubic complexity. The main algorithm for deduction search is described in the third chapter. It is shown that derivation in multilevel logics with linear order has some particularities in comparison with derivation in classic logic, concerning preferences of inference rule application. Some methods for inference rule searching and for optimization of deduction process are also proposed in this work.

Abstract (fr) | Abstract (rus) | ASDS demo [ZIP, 352K]