In this paper we deepen Mundici's analysis on reducibility of the decision problem from infinite-valued ukasiewicz logic to a suitable m-valued ukasiewicz logic m , where m only depends on the length of the formulas to be proved. Using geometrical arguments we find a better upper bound for the least integer m such that a formula is valid in if and only if it is also valid in m. We also reduce the notion of logical consequence in to the same (...) notion in a suitable finite set of finite-valued ukasiewicz logics. Finally, we define an analytic and internal sequent calculus for infinite-valued ukasiewicz logic. (shrink)

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.

Angell's logic of analytic containment AC has been shown to be characterized by a 9-valued matrix NC by Ferguson, and by a 16-valued matrix by Fine. We show that the former is the image of a surjective homomorphism from the latter, i.e., an epimorphic image. The epimorphism was found with the help of MUltlog, which also provides a tableau calculus for NC extended by quantifiers that generalize conjunction and disjunction.

The closed world assumption plays a fundamental role in the theory of deductive databases. On the other hand, multi-valued logics occupy a vast field in non-classical logics. Some questions are better explained and expressed in terms of such logics. To enhance the expressive power and the declarative ability of a deductive database, we extend various CWA formalizations, including the naive CWA, the generalized CWA and the careful CWA, to multi-valued logics. The basic idea is to embed logic formulae into some (...) polynomial ring. The extensions can be applied in a uniform manner to any finitely multi-valued logics. Therefore they have also computational interest. (shrink)

ABSTRACT We show that there is a polynomial over the rational number field corresponding to each propositional formula in a given many-valued logic. To decide whether a propositional formula can be deduced from a finite set of such formulas (deduction problem), we only need to decide whether a polynomial vanishes on an algebraic variety. By using Wu's method, an algorithm for this problem is presented.

ABSTRACT We are concerned with the theorem proving in annotated logics. By using annotated polynomials to express knowledge, we develop an inference rule superposition. A proof procedure is thus presented, and an improvement named M- strategy is mainly described. This proof procedure uses single overlaps instead of multiple overlaps, and above all, both the proof procedure and M-strategy are refutationally complete.

(2012). Reasoning without believing: on the mechanisation of presuppositions and partiality. Journal of Applied Non-Classical Logics: Vol. 22, No. 4, pp. 295-317. doi: 10.1080/11663081.2012.705962.