Development and implementation of algorithms for data processing in multivalued logics
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]