
doi: 10.1007/bf01058388
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.
Mechanization of proofs and logical operations, linear programming applications, theorem proving, computational complexity, algorithm, Many-valued logic, decision procedures, \(\aleph_ 0\)-valued Łukasiewicz logic, Theorem proving (deduction, resolution, etc.), theoremhood
Mechanization of proofs and logical operations, linear programming applications, theorem proving, computational complexity, algorithm, Many-valued logic, decision procedures, \(\aleph_ 0\)-valued Łukasiewicz logic, Theorem proving (deduction, resolution, etc.), theoremhood
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
