A Parigot-style linear -calculus for full intuitionistic linear logic.
We obtain a principal topology and some related results. We also give some hints of possible applications. Some mathematical systems are both lattice and topological space. We show that a topology defined on the any bounded lattice is definable in terms of uninorms. Also, we see that these topologies satisfy the condition of the principal topology. These topologies can not be metrizable except for the discrete metric case. We show an equivalence relation on the class of uninorms on a bounded lattice...
It is shown that in a finitely decidable equational class, the solvable radical of any finite subdirectly irreducible member is comparable to all congruences of the irreducible if the type of the monolith is 2. In the type 1 case we establish that the centralizer of the monolith is strongly solvable.
We present a new prover for propositional 3-valued logics, TAS-M3, which is an extension of the TAS-D prover for classical propositional logic. TAS-M3 uses the TAS methodology and, consequently, it is a reduction-based method. Thus, its power is based on the reductions of the size of the formula executed by the F transformation. This transformation dynamically filters the information contained in the syntactic structure of the formula to avoid as much distributions as possible, in order to improve...
In this paper a semantical partition, relative to Kripke models, is introduced for sets of formulas. Secondly, this partition is used to generate a semantical hierarchy for modal formulas. In particular some results are given for the propositional calculi T and S4.
The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model's behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process inference is...
Several transformation which enable implication functions in multivalued logics to be generated from conjunctions have been proposed in the literature. It is proved that for a rather general class of conjunctions modeled by triangular norms, the generation process is closed, thus shedding some light on the relationships between seemingly independent classes of implication functions.
In this paper a fuzzy relation-based framework is shown to be suitable to describe not only knowledge-based medical systems, explicitly using fuzzy approaches, but other ways of knowledge representation and processing. A particular example, the practically tested medical expert system Disco, is investigated from this point of view. The system is described in the fuzzy relation-based framework and compared with CADIAG-II-like systems that are a “pattern” for computer-assisted diagnosis systems based...