Arnon Avron

FLAP Journal 2025 Journal Article

The Influence of Dov on My Work

• Arnon Avron

FLAP Journal 2019 Journal Article

Reasoning about Covering-based Rough Sets Using Three Truth Values.

• Beata Konikowska
• Arnon Avron

The paper presents a natural three-valued logic for reasoning about coveringbased rough sets. Atomic formulas of the logic represent membership of objects of the universe in rough sets, and complex formulas are built out of the atomic ones using three-valued Kleene connectives. To reflect the structure of rough sets, semantics of the logic employs three truth values: t — representing truth and corresponding to membership of an object in the positive region of a set, f — representing falsity and corresponding to membership in the negative region, and u — representing undefinedness (lack of information) and corresponding to membership in the boundary region of the set. In the paper we provide a finitely strongly sound and complete Gentzen-style sequent calculus for the described logic.

CSL Conference 2018 Conference Paper

Safety, Absoluteness, and Computability

• Arnon Avron
• Shahar Lev
• Nissan Levi

The semantic notion of dependent safety is a common generalization of the notion of absoluteness used in set theory and the notion of domain independence used in database theory for characterizing safe queries. This notion has been used in previous works to provide a unified theory of constructions and operations as they are used in different branches of mathematics and computer science, including set theory, computability theory, and database theory. In this paper we provide a complete syntactic characterization of general first-order dependent safety. We also show that this syntactic safety relation can be used for characterizing the set of strictly decidable relations on the natural numbers, as well as for characterizing rudimentary set theory and absoluteness of formulas within it.

FLAP Journal 2017 Journal Article

Cut-elimination in RM Proved Semantically.

• Arnon Avron

A purely semantic proof is presented for the admissibility of the Cut rule in the hypersequential Gentzen-type system for RM.

IJCAI Conference 2011 Conference Paper

What Is an Ideal Logic for Reasoning with Inconsistency?

• Ofer Arieli
• Arnon Avron
• Anna Zamansky

Many AI applications are based on some underlying logic that tolerates inconsistent information in a non-trivial way. However, it is not always clear what should be the exact nature of such a logic, and how to choose one for a specific application. In this paper, we formulate a list of desirable properties of `ideal' logics for reasoning with inconsistency, identify a variety of logics that have these properties, and provide a systematic way of constructing, for every n > 2, a family of such n-valued logics.

KR Conference 2010 Conference Paper

Maximally Paraconsistent Three-Valued Logics

• Ofer Arieli
• Arnon Avron
• Anna Zamansky

Maximality is a desirable property of paraconsistent logics, motivated by the aspiration to tolerate inconsistencies, but at the same time retain from classical logic as much as possible. In this paper, we introduce the strongest possible notion of maximal paraconsistency, and investigate it in the context of logics that are based on deterministic or non-deterministic three-valued matrices. We first show that most of the logics that are based on properly non-deterministic three-valued matrices are not maximally paraconsistent. Then we show that in contrast, in the deterministic case all the natural three-valued paraconsistent logics are maximal. This includes well-known three-valued paraconsistent logics like P1, LP, J3, PAC and SRM3, as well as any extension of them obtained by enriching their languages with extra three-valued connectives. In this paper, we investigate strong maximality of paraconsistent logics based on three-valued deterministic and non-deterministic matrices. The former are one of the oldest and most common ways of defining a paraconsistent logic. The latter are a recent natural generalization of the former, introduced in (Avron and Lev 2005), in which nondeterministic interpretations of connectives are allowed. Under a very minimal and natural assumption about the interpretation of negation in these matrices, we show that in the deterministic case, all natural three-valued paraconsistent logics are maximal in the strong sense. Our result applies to such well-known paraconsistent logics as Sette’s logic P1, Priest’s LP, the semi-relevant logic SRM3, the logics PAC and J3, and any extension of one of these logics obtained by enriching its language with extra three-valued connectives. 1 In the non-deterministic case things are quite different, though. We show that paraconsistent logics induced by properly non-deterministic three-valued matrices are usually not maximal, except for a few special cases (which are fully characterized). However, even these exceptional cases are redundant, as we show that any maximally paraconsistent logic defined by an n-valued non-deterministic matrix can be fully characterized also by a deterministic one.

TCS Journal 2008 Journal Article

Constructibility and decidability versus domain independence and absoluteness

• Arnon Avron

We develop a unified framework for dealing with constructibility and absoluteness in set theory, decidability of relations in effective structures (like the natural numbers) and domain independence of queries in database theory. Our framework and results suggest that domain-independence and absoluteness might be the key notions in a general theory of constructibility, predicativity and computability.

KR Conference 2006 Conference Paper

Non-deterministic semantics for first-order paraconsistent logics

• Arnon Avron
• Anna Zamansky

Using non-deterministic structures called Nmatrices, we provide simple modular non-deterministic semantics for a large family of first-order paraconsistent logics with a formal consistency operator, also known as LFIs. This includes da-Costa's well known predicate calculus C*1. We show how consistency propagation in quantified formulas is captured in the semantic framework of Nmatrices, and analyze the semantic effects of different styles of propagation considered in the literature of LFIs. Then we demonstrate how the tool of Nmatrices can be applied to prove a non-trivial property of first-order LFIs discussed in this paper.

AIJ Journal 1998 Journal Article

The value of the four values

• Ofer Arieli
• Arnon Avron

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.

CSL Conference 1997 Conference Paper

Four-Valued Diagnoses for Stratified Knowledge-Bases

• Ofer Arieli
• Arnon Avron

Abstract We present a four-valued approach for recovering consistent data from inconsistent set of assertions. For a common family of knowledge-bases we also provide an efficient algorithm for doing so automaticly. This method is particularly useful for making model-based diagnoses.

I&C Journal 1991 Journal Article

Simple consequence relations

• Arnon Avron

We provide a general investigation of logic in which the notion of a simple consequence relation is taken to be fundamental. Our notion is more general than the usual one since we give up monotonicity and use multisets rather than sets. We use our notion to characterize several known logics (including linear logic and non-monotonic logics) and for a general, semantics-independent classification of standard onnectives via equations on consequence relations (these include Girard's “multiplicatives” and “additives”). We next investigate the standard methods for uniformly representing consequence relations: Hilbert type, Natural Deduction, and Gentzen type. The advantages and disadvantages of using each system and what should be taken as good representations in each case (especially from the implementation point of view) are explained. We end by briefly outlining (with examples) some methods for developing non-uniform, but still efficient, representations of consequence relations.

TCS Journal 1988 Journal Article

The semantics and proof theory of linear logic

• Arnon Avron

Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in [9]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding Strong completeness theorems. Finally, we shall investigate the relation between Linear Logic and previously known systems, especially Relevance Logics.