Automated theorem proving for Łukasiewicz logics (Q687151)

The paper is concerned with decision procedures for the \(\aleph_ 0\)- valued Łukasiewicz logic \(L_{\aleph_ 0}\). Within the paper, the author presents an attempt to use linear programming techniques in theorem provers for the \(\aleph_ 0\)-valued Łukasiewicz logics. In the first part, some convenient linear algebraic framework for Łukasiewicz logics is developed: a series of basic concepts, operators and decision algorithms to verify the theoremhood property for different formulae are presented here. Next, some additional binary connectives are introduced and reasoning schemes are expressed in terms of the previously considered formalism. An interesting method to check if a formula is a logical consequence of a set of formulas is presented in the sixth section. Finally, some arguments concerning the corresponding computational complexity of the proposed algorithm are supplied.