A family of Gödel hybrid logics

In this paper, we define a family of fuzzy hybrid logics that are based on Gödel logic. It is composed of two infinite-valued versions called ${\mathsf{GH}}_{\infty }$ and ${\mathsf{WGH}}_{\infty }$, and a sequence of finitary valued versions ${({\mathsf{GH}}_n)}_{0<n<\infty }$. We define decision procedures for both ${\mathsf{WGH}}_{\infty }$ and ${({\mathsf{GH}}_n)}_{0<n<\infty }$ that are based on particular sequents and on a set of proof rules dealing with such sequents. As these rules are strongly invertible the procedures naturally allow one to generate countermodels. Therefore we prove the decidability and the finite model property for these logics. Finally, from the decision procedure of ${\mathsf{WGH}}_{\infty }$, we design a sound and complete sequent calculus for this logic.     

Tableau reductions: Towards an optimal decision procedure for the modal necessity

We present a new prefixed tableau system $\mathsf{TK}$ for verification of validity in modal logic $\mathsf{K}$. The system $\mathsf{TK}$ is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. $\mathsf{TK}$ is defined in the original methodology of tableau systems, without any external technique such as backtracking, backjumping, etc. Since all the necessary bookkeeping is built into the rules, the system is not only a basis for a validity algorithm, but is itself a decision procedure. We present also a deterministic tableau decision procedure which is an extension of $\mathsf{TK}$ and can be used for the global assumptions problem.     

Combining linear-time temporal logic with constructiveness and paraconsistency

It is known that linear-time temporal logic (LTL), which is an extension of classical logic, is useful for expressing temporal reasoning as investigated in computer science. In this paper, two constructive and bounded versions of LTL, which are extensions of intuitionistic logic or Nelson's paraconsistent logic, are introduced as Gentzen-type sequent calculi. These logics, $\mathrm{IB}[l]$ and $\mathrm{PB}[l]$, are intended to provide a useful theoretical basis for representing not only temporal (linear-time), but also constructive, and paraconsistent (inconsistency-tolerant) reasoning. The time domain of the proposed logics is bounded by a fixed positive integer. Despite the restriction on the time domain, the logics can derive almost all the typical temporal axioms of LTL. As a merit of bounding time, faithful embeddings into intuitionistic logic and Nelson's paraconsistent logic are shown for $\mathrm{IB}[l]$ and $\mathrm{PB}[l]$, respectively. Completeness (with respect to Kripke semantics), cut–elimination, normalization (with respect to natural deduction), and decidability theorems for the newly defined logics are proved as the main results of this paper. Moreover, we present sound and complete display calculi for $\mathrm{IB}[l]$ and $\mathrm{PB}[l]$.In [P. Maier, Intuitionistic LTL and a new characterization of safety and liveness, in: Proceedings of Computer Science Logic 2004, in: Lecture Notes in Computer Science, vol. 3210, Springer-Verlag, Berlin, 2004, pp. 295–309] it has been emphasized that intuitionistic linear-time logic (ILTL) admits an elegant characterization of safety and liveness properties. The system ILTL, however, has been presented only in an algebraic setting. The present paper is the first semantical and proof-theoretical study of bounded constructive linear-time temporal logics containing either intuitionistic or strong negation.