Search

In this study, we prove the completeness and cut-elimination theorems for a first-order extension F4CC of Arieli, Avron, and Zamansky’s ideal paraconsistent four-valued logic known as 4CC. These theorems are proved using Schutte’s method, which can simultaneously prove completeness and cut-elimination.

The four-valued semantics of Belnap–Dunn logic, consisting of the truth values True, False, Neither, and Both, gives rise to several nonclassical logics depending on which feature of propositions we wish to preserve: truth, nonfalsity, or exact truth (truth and nonfalsity). Interpreting equality of truth values in this semantics as material equivalence of propositions, we can moreover see the equational consequence relation of this four-element algebra as a logic of material equivalence. In this paper, we axiomatize all combinations of these four-valued logics, for example, the logic of truth and exact truth or the logic of truth and material equivalence. These combined systems are consequence relations which allow us to express implications involving more than one of these features of propositions.

A modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC is introduced as a Gentzen-type sequent calculus. The completeness theorem with respect to a Kripke semantics for M4CC is proved. The finite model property for M4CC is shown by modifying the completeness proof. The decidability of M4CC is obtained as a corollary.

In this paper, we consider a set of quite interesting three- and four-valued logics and prove the normalisation theorem for their natural deduction formulations. Among the logics in question are the Logic of Paradox, First Degree Entailment, Strong Kleene logic, and some of their implicative extensions, including RM3 and RM3⊃. Also, we present a detailed version of Prawitz’s proof of Nelson’s logic N4 and its extension by intuitionist negation.

This study aims to introduce a modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC as a Gentzen-type sequent calculus and prove the Kripke-completeness and cut-elimination theorems for M4CC. The logic M4CC is also shown to be decidable and embeddable into the normal modal logic S4. Furthermore, a subsystem of M4CC, which has some characteristic properties that do not hold for M4CC, is introduced and the Kripke-completeness and cut-elimination theorems for this subsystem are proved. This subsystem is also shown to be decidable and embeddable into S4.

We introduce a novel expansion of the four-valued Belnap---Dunn logic by a unary operator representing reductio ad contradictionem and study its algebraic semantics. This expansion thus contains both the direct, non-inferential negation of the Belnap---Dunn logic and an inferential negation akin to the negation of Johansson's minimal logic. We formulate a sequent calculus for this logic and introduce the variety of reductio algebras as an algebraic semantics for this calculus. We then investigate some basic algebraic properties of this variety, in particular we show that it is locally finite and has EDPC. We identify the subdirectly irreducible algebras in this variety and describe the lattice of varieties of reductio algebras. In particular, we prove that this lattice contains an interval isomorphic to the lattice of classes of finite non-empty graphs with loops closed under surjective graph homomorphisms.

We have recently developed a package in Maple that allows to perform logical computations in any existing or proposed many-valued logic (that can be defined using truth tables). It has applications in logic engineering (e.g. when creating a new logic adapted to some requirements), in theoretical logic (e.g. checking if two axiomatizations of a logic are equivalent), or simply in checking the properties of a well known logic. Now, such a package has been tuned so that it can simultaneously deal with the logic proposed by the end user plus the standard Boolean logic, in order to conveniently check properties. This new approach is used to easily develop some disquisitions on why Belnap's four-valued logic is defined the way it is. Finally, it is shown how a new four valued logic that mixes ideas from Łukasiewicz's and Kleene's logics behaves similarly to Belnap's logic.

Here, I first prove that certain families of k-valued clones have the Gupta-Belnap fixed-point property. This essentially means that all propositional languages that are interpreted with operators belonging to those clones are such that any net of self-referential sentences in the language can be consistently evaluated. I then focus on two four-valued generalisations of the Kleene propositional operators that generalise the strong and weak Kleene operators: Belnap’s clone and Fitting’s clone, respectively. I apply the theorems from the initial part of the paper to analyse the fixed-point property of Belnap’s and Fitting’s clones when some special operators that reflect the semantics are added. The conclusion of the paper is that Fitting’s clone is better suited than Belnap’s to provide self-referential languages with highly expressive resources.

In their recent paper Bi-facial truth: a case for generalized truth values Zaitsev and Shramko [7] distinguish between an ontological and an epistemic interpretation of classical truth values. By taking the Cartesian product of the two disjoint sets of values thus obtained, they arrive at four generalized truth values and consider two “semi-classical negations” on them. The resulting semantics is used to define three novel logics which are closely related to Belnap’s well-known four valued logic. A syntactic characterization of these logics is left for further work. In this paper, based on our previous work on a functionally complete extension of Belnap’s logic, we present a sound and complete tableau calculus for these logics. It crucially exploits the Cartesian nature of the four values, which is reflected in the fact that each proof consists of two tableaux. The bi-facial notion of truth of Z&S is thus augmented with a bi-facial notion of proof. We also provide translations between the logics for semi-classical negation and classical logic and show that an argument is valid in a logic for semi-classical negation just in case its translation is valid in classical logic.

The development of recursion theory motivated Kleene to create regular three-valued logics. Remove it taking his inspiration from the computer science, Fitting later continued to investigate regular three-valued logics and defined them as monotonic ones. Afterwards, Komendantskaya proved that there are four regular three-valued logics and in the three-valued case the set of regular logics coincides with the set of monotonic logics. Next, Tomova showed that in the four-valued case regularity and monotonicity do not coincide. She counted that there are 6400 four-valued regular logics, but only six of them are monotonic. The purpose of this paper is to create natural deduction systems for them. We also describe some functional properties of these logics.

In the structure theory of many-valued logic function, the decision and constitution of the Sheffer function is a very important problem, which is reduced to the decision of the minimal covering of precomplete sets in the many-valued logic function sets. According to the completeness theory in partial k-valued logic and the similar relationship theory among precomplete sets, in this paper, the methods of determination on the minimal covering of regular separable function sets are found out, and the minimal covering of regular separable function sets in partial four-valued logic are decided.

The trilattice \(\textit{SIXTEEN}_3\) is a natural generalization of the well-known bilattice \(\textit{FOUR}_2\). Cut-free, sound and complete sequent calculi for truth entailment and falsity entailment in \(\textit{SIXTEEN}_3\) are presented.

In answer set programming, an extended logic program may have no answer set, or only one trivial answer set. In this paper, we propose a new stable model semantics based on the restricted four-valued logic to overcome both inconsistences and incoherences in answer set programming. Our stable models coincide with classical answer sets when reasoning on consistent and coherent logic programs, and can be solved by transformation in existing ASP solvers. We also show the connection between our stable models and the extensions of default logic.

Based on the semantic concepts developed by M.~Dunn and N.~Belnap, a four-valued language containing only two logical symbols is proposed. We show that this language is functionally complete with regard to the given semantics. Specifically, we prove that every truth-function is expressed by a formula of the language. To do this, we define two concepts akin to the disjunctive and conjunctive normal forms. Using these concepts, we establish that every truth-function for a four-valued semantics can be represented by a formula in a disjunctive form or in a conjunctive form.

This chapter aims to investigate connections between Belnap’s useful four valued logic and Nelson’s constructive logic with strong negation and the role of adding logical constants to the language. We consider the paraconsistent Nelson’s logic and its expansions obtained by adding to it logical constant’s corresponding to truth values of Belnap’s useful four-valued logic.

Łukasiewicz's four-valued modal logic is surveyed and analyzed, together with Łukasiewicz's motivations to develop it. A faithful interpretation of it in classical (non-modal) two-valued logic is presented, and some consequences are drawn concerning its classification and its algebraic behaviour. Some counter-intuitive aspects of this logic are discussed in the light of the presented results, Łukasiewicz's own texts, and related literature.

We propose a combination of a fragment of four-valued logic and process algebra. We present an operational semantics in SOS-style, and a completeness result for ACP with conditionals and four-valued logic.

In this paper we study 12 four-valued logics arisen from Belnap's truth and/or knowledge four-valued lattices, with or without constants, by adding one or both or none of two new non-regular operations—classical negation and natural implication. We prove that the secondary connectives of the bilattice four-valued logic with bilattice constants are exactly the regular four-valued operations. Moreover, we prove that its expansion by any non-regular connective (such as, e.g., classical negation or natural implication) is strictly functionally complete. Further, finding axiomatizations of the quasi varieties generated by the 12 logics involved (that prove to be varieties), we find naturell equational axiomatizations of these logics. Finally, applying Pynko's general theory of algebraizable sequential consequence operations, we also find equivalent natural sequentiell axiomatizations of the logics under consideration that expand either of two Pynko's sequential calculi for the constant-free truth-latt...

The paper presents some new results concerning the axiomatization of double threshold preference structures. Such structures, which have been introduced in order to model a situation of hesitation between the strict preference and the indifference, were not axiomatized through the use of a single characteristic relation. We give two theorems for this purpose, exploiting a four valued logic recently introduced by the authors as a preference modeling language under hesitation. © 1998 John Wiley & Sons, Ltd., FLWIN, SCOPUS: ar.j, info:eu-repo/semantics/published

There are various approaches to develop a system of paraconsistent logic, and those we focus on in this paper are approaches of da Costa, Belnap, and Nelson. Our main focus is da Costa, and we deal with a system that reflects the idea of da Costa. We understand that the main idea of da Costa is to make explicit, within the system, the area in which you can infer classically. The aim of the paper is threefold. First, we introduce and present some results on a classicality operator which generalizes the consistency operator of Logics of Formal Inconsistency. Second, we show that we can introduce the classicality operator to the systems of Belnap. Third, we demonstrate that we can generalize the classicality operator above to the system of Nelson. The paper presents both the proof theory and semantics for the systems to be introduced, and also establishes some completeness theorems.

The paper presents some results obtained in searching for a new axiomatic foundation for partial comparability (PC) in the frame of non-conventional preference modeling. The basic idea is to define an extended preference structure able to represent lack of information, uncertainty, ambiguity, multidimensional and conflicting preferences, using formal logic as the basic formalism. A four-valued paraconsistent logic is therefore described in the paper as a more suitable language for the purposes of the research. The concepts of partition, general binary relations properties, fundamental relational system of preferences (f.r.s.p.), maximal f.r.s.p. and well founded f.r.s.p. are then introduced and some theorems are demonstrated in order to provide the axiomatic foundation of PC. The main result obtained is a preference structure that is a maximal well founded f.r.s.p. This preference structure facilitates a more flexible, reliable and robust preference modeling. Moreover it can be viewed as a generalization of the conventional approach, so that all the results obtained until now can be used under it. Two examples are provided at the end of the paper in order to give an account of the operational potentialities of the new theory, mainly in the area of multicriteria decision aid and social choice theory. Further research directions conclude the paper.

When monitoring a system w.r.t. a property defined in a temporal logic such as LTL, a major concern is to settle with an adequate interpretation of observable system events; that is, models of temporal logic formulae are usually infinite words of events, whereas at runtime only finite but incrementally expanding prefixes are available.In this work, we review LTL-derived logics for finite traces from a runtime-verification perspective. In doing so, we establish four maxims to be satisfied by any LTL-derived logic aimed at runtime verification. As no pre-existing logic readily satisfies all of them, we introduce a new four-valued logic Runtime Verification Linear Temporal Logic RV-LTL in accordance to these maxims. The semantics of Runtime Verification Linear Temporal Logic (RV-LTL) indicates whether a finite word describes a system behaviour which either (i) satisfies the monitored property, (ii) violates the property, (iii) will presumably violate the property, or (iv) will presumably conform to the property in the future, once the system has stabilized. Notably, (i) and (ii) correspond to the classical semantics of LTL, whereas (iii) and (iv) are chosen whenever an observed system behaviour has not yet lead to a violation or acceptance of the monitored property.Moreover, we present a monitor construction for RV-LTL properties in terms of Moore machines signalizing the semantics of the so far obtained execution trace w.r.t. the monitored property. © The Author, 2010. Published by Oxford University Press. All rights reserved.

In many-valued logic theories, the decision and construction for Sheffer functions is an important problem. The decision for Sheffer functions is interrelated to the decision for completeness of functions set, and the solution can be reduced to determining the minimal coverings of precomplete. It's well known that each precomplete set is a function set, T(G m ) , preserving the relation G m , therefore, the categorizing of this relation has provided the determination of precomplete set's minimal covering with more convenient ways. In this paper, preserving quaternary regularly separable relations in partial four-valued logic are categorized by similar relation.

Bilattices, due to M. Ginsberg, are a family of truth-value spaces that allow elegantly for missing or conflicting information. The simplest example is Belnap's four-valued logic, based on classical two-valued logic. Among other examples are those based on finite many-valued logics and on probabilistic-valued logic. A fixed-point semantics is developed for logic programming, allowing any bilattice as the space of truth values. The mathematics is little more complex than in the classical two-valued setting, but the result provides a natural semantics for distributed logic programs, including those involving confidence factors. The classical two-valued and the Kripke-Kleene three-valued semantics become special cases, since the logics involved are natural sublogics of Belnap's logic, the logic given by the simplest bilattice.

This report deals with the application of multi-valued logic in cellular automata. A four valued logic system with dibit representation has been considered in this case. The general properties and their relations to build such logical systems are also investigated and the question of implementation of this logical system in cellular automata environment has also been studied. It is shown, that chaotic fractals i.e, fractals as function of initial conditions are formed in such cases. It is interesting to note also that fractals so formed are multifractals and thus may have applications in analyzing natural fractal formation. Subject. terms: Multivalued Logic, Cellular Automata, Fractals.

In multiple-valued logic theories, the decision and construction for Sheffer functions is an important problem. The decision for Sheffer functions is interrelated to the decision for completeness of functions set, and the solution can be reduced to determining the minimal coverings of precomplete. It's well known that each precomplete set is a function set,T(Gm), preserving the relation Gm, therefore, the categorizing of this relation has provided the determination of precomplete set's minimal covering with more convenient ways. In this paper, fully symmetric relations in partial four-valued logic are categorized by similar relation.

In completeness theories of multiple-valued logic, the characterization of Sheffer functions is an important problem, and the solution can be reduced to determining the minimal coverings of precomplete categories. It'fs well known that each precomplete set is a function set, T(Gm), preserving the relation Gm, therefore, the categorizing of this relation has provided the determination of precomplete set's minimal covering with more convenient ways. In this paper, simply separable relations in partial four-valued logic are categorized by similar relation.

The author discusses a four-valued logic using two lines each of which consists of two-valued logical elements. It is obtained by adding a few monomial operators to the operators of the four-valued logic reported by T. Chen et al. (1983). Functional completeness, duality, canonical form, simplification and other theorems are discussed. It is concluded that the functional space of four-valued logic is equivalent to that of two-valued logic. It is also found that variables and operators of modal logic correspond to those of four-valued logic using two lines. >

A four-valued logic defined by the four-element De Morgan lattice together with its two prime filters is treated. For certain classes of abstract logics, several characterizations in terms of De Morgan lattices and projective generation of logics by sets of homomorphisms or by a single epimorphism (a biological morphism) are described. A similar treatment is shown for the three-valued logic generated by the three-element chain together with its two prime filters, and for the incorporation of the falsum connective, which brings out the classes of all De Morgan algebras and all Kleene algebras. >

In this paper, the application of a four-valued logic to the switch-level test generation is studied. A switch-level operator fault model is proposed. Switch-level U difference and Z difference of a function to a fault are defined. A method to derive switch-level differences is given. Finally, a new switch-level test generation algorithm for CMOS circuits is presented. >

International audience; The principle of concordance/discordance was introduced by B. Roy in his very early work on Multiple Criteria Decision Analysis. Although such a principle is grounded by strong evidence from real life decision situations, the way in which it has been implemented in existing MCDA methods allows only for its partial and limited use. Indeed, the principle lacks a theoretical frame enabling a more general use in decision analysis. The paper presents a possible generalisation of this principle under the concepts of positive and negative reasons. For this purpose, a new formalism, (a four valued logic) is suggested. Under such a formalism the concordance test is seen as the evaluation of the existence of positive reasons supporting the sentence “x is at least as good as y”, while the discordance test can be viewed as the evaluation of the existence of negative reasons against the same sentence. A number of results obtained in preference modelling and aggregation shows the potentiality of this approach.

International audience; It has long been recognized that the concept of inconsistency is a central part of com-monsense reasoning. In this issue, a number of authors have explored the idea of reasoning with maximal consistent subsets of an inconsistent stratified knowledge base. This paradigm, often called "coherent-based reasoning", has resulted in some interesting proposals for para-consistent reasoning, non-monotonic reasoning, and argumentation systems. Unfortunately, coherent-based reasoning is computationally very expensive. This paper harnesses the approach of approximate entailment by Schaerf and Cadoli [SCH 95] to develop the concept of "approximate coherent-based reasoning". To this end, we begin to present a multi-modal propo-sitional logic that incorporates two dual families of modalities: 2S and 3S defined for each subset S of the set of atomic propositions. The resource parameter S indicates what atoms are taken into account when evaluating formulas. Next, we define resource-bounded consolidation operations that limit and control the generation of maximal consistent subsets of a stratified knowledge base. Then, we present counterparts to existential, universal, and argumentative inference that are prominent in coherence-based approaches. By virtue of modalities 2S and 3S, these inferences are approximated from below and from above, in an incremental fashion. Based on these features, we show that an anytime view of coherent-based reasoning is tenable.

We introduce a four‐valued logic that includes, in addition to true and false, the values unknown and non‐existent. We introduce the idea of presupposition in fuzzy logic and then use this to relate this four valued logic to the binary logic.

In his well-known paper “How computer should think” Belnap (1977) argues that four-valued semantics is a very suitable setting for computerized reasoning. In this paper we vindicate this thesis by showing that the logical role that the four-valued structure has among Ginsberg's bilattices is similar to the role that the two-valued algebra has among Boolean algebras. Specifically, we provide several theorems that show that the most useful bilattice-valued logics can actually be characterized as four-valued inference relations. In addition, we compare the use of three-valued logics with the use of four-valued logics, and show that at least for the task of handling inconsistent or uncertain information, the comparison is in favor of the latter.

Bilattices and d-frames are two different kinds of structures with a four-valued interpretation. Whereas d-frames were introduced with their topological semantics in mind, the theory of bilattices has a closer connection with logic. We consider a common generalisation of both structures and show that this not only still has a clear bitopological semantics, but that it also preserves most of the original bilattice logic. Moreover, we also obtain a new bitopological interpretation for the connectives of four-valued logic.

Belnap offers two arguments for the usefulness of four-valued logic. I argue that one of them, which rests on interpreting valuations as states of our information, when taken seriously collapses into an argument for two-valued logic in which relevance is lost, and that the other, resting on Scott's thesis, is not an argument for its usefulness