Order:
Disambiguations
Arnon Avron [75]A. Avron [9]
See also
Arnon Avron
Tel Aviv University
  1.  27
    Reasoning with Logical Bilattices.Ofer Arieli & Arnon Avron - 1996 - Journal of Logic, Language and Information 5 (1):25--63.
    The notion of bilattice was introduced by Ginsberg, and further examined by Fitting, as a general framework for many applications. In the present paper we develop proof systems, which correspond to bilattices in an essential way. For this goal we introduce the notion of logical bilattices. We also show how they can be used for efficient inferences from possibly inconsistent data. For this we incorporate certain ideas of Kifer and Lozinskii, which happen to suit well the context of our work. (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   57 citations  
  2. Simple Consequence Relations.Arnon Avron - unknown
    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 for characterizing several known logics (including Linear Logic and non-monotonic logics) and for a general, semantics-independent classi cation of standard connectives via equations on consequence relations (these include Girard's \multiplicatives" and \additives"). We next investigate the (...)
     
    Export citation  
     
    Bookmark   23 citations  
  3. The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics.Arnon Avron - unknown
    Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by many researchers (...)
     
    Export citation  
     
    Bookmark   19 citations  
  4.  40
    Natural 3-Valued Logics—Characterization and Proof Theory.Arnon Avron - 1991 - Journal of Symbolic Logic 56 (1):276-294.
  5. Non-Deterministic Matrices and Modular Semantics of Rules.Arnon Avron - unknown
    We show by way of example how one can provide in a lot of cases simple modular semantics for rules of inference, so that the semantics of a system is obtained by joining the semantics of its rules in the most straightforward way. Our main tool for this task is the use of finite Nmatrices, which are multi-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set (...)
     
    Export citation  
     
    Bookmark   15 citations  
  6.  66
    Ideal Paraconsistent Logics.O. Arieli, A. Avron & A. Zamansky - 2011 - Studia Logica 99 (1-3):31-60.
    We define in precise terms the basic properties that an ‘ideal propositional paraconsistent logic’ is expected to have, and investigate the relations between them. This leads to a precise characterization of ideal propositional paraconsistent logics. We show that every three-valued paraconsistent logic which is contained in classical logic, and has a proper implication connective, is ideal. Then we show that for every n > 2 there exists an extensive family of ideal n -valued logics, each one of which is not (...)
    Direct download (7 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   10 citations  
  7.  8
    Multi-Valued Calculi for Logics Based on Non-Determinism.Arnon Avron & Beata Konikowska - 2005 - Logic Journal of the IGPL 13 (4):365-387.
    Non-deterministic matrices are multiple-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set of options. We consider two different types of semantics which are based on Nmatrices: the dynamic one and the static one . We use the Rasiowa-Sikorski decomposition methodology to get sound and complete proof systems employing finite sets of mv-signed formulas for all propositional logics based on such structures with either of the above (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  8.  58
    The Semantics and Proof Theory of Linear Logic.Arnon Avron - 1988 - Theoretical Computer Science 57:161-184.
    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 Gi]. 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 str ong completeness theorems. Finally, we shall investigate (...)
    Direct download  
     
    Export citation  
     
    Bookmark   33 citations  
  9.  51
    What is Relevance Logic?Arnon Avron - 2014 - Annals of Pure and Applied Logic 165 (1):26-48.
    We suggest two precise abstract definitions of the notion of ‘relevance logic’ which are both independent of any proof system or semantics. We show that according to the simpler one, R → source is the minimal relevance logic, but R itself is not. In contrast, R and many other logics are relevance logics according to the second definition, while all fragments of linear logic are not.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  10. Non-Deterministic Semantics for Logics with a Consistency Operator.Arnon Avron - unknown
    In order to handle inconsistent knowledge bases in a reasonable way, one needs a logic which allows nontrivial inconsistent theories. Logics of this sort are called paraconsistent. One of the oldest and best known approaches to the problem of designing useful paraconsistent logics is da Costa’s approach, which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. Da Costa’s approach has led to the family of logics (...)
    Translate
     
     
    Export citation  
     
    Bookmark   10 citations  
  11. A Constructive Analysis of RM.Arnon Avron - 1987 - Journal of Symbolic Logic 52 (4):939 - 951.
  12.  16
    Maximal and Premaximal Paraconsistency in the Framework of Three-Valued Semantics.Ofer Arieli, Arnon Avron & Anna Zamansky - 2011 - Studia Logica 97 (1):31 - 60.
    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 show that all reasonable paraconsistent logics based on three-valued deterministic matrices are maximal in our strong sense. This applies to practically all three-valued (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  13. Cut-Elimination and Quantification in Canonical Systems.Anna Zamansky & Arnon Avron - 2006 - Studia Logica 82 (1):157-176.
    Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  14.  13
    John C. Mitchell. Foundations for Programming Languages. Foundations of Computing. The MIT Press, Cambridge, Mass., and London, 1996, Xix + 846 Pp. [REVIEW]Arnon Avron - 1999 - Journal of Symbolic Logic 64 (2):918-922.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  15.  19
    Paraconsistency, Paracompleteness, Gentzen Systems, and Trivalent Semantics.Arnon Avron - 2014 - Journal of Applied Non-Classical Logics 24 (1-2):12-34.
    A quasi-canonical Gentzen-type system is a Gentzen-type system in which each logical rule introduces either a formula of the form , or of the form , and all the active formulas of its premises belong to the set . In this paper we investigate quasi-canonical systems in which exactly one of the two classical rules for negation is included, turning the induced logic into either a paraconsistent logic or a paracomplete logic, but not both. We provide a constructive coherence criterion (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  16.  36
    On an Implication Connective of RM.Arnon Avron - 1986 - Notre Dame Journal of Formal Logic 27 (2):201-209.
  17. Gentzen-Type Systems, Resolution and Tableaux.Arnon Avron - unknown
    In advanced books and courses on logic (e.g. Sm], BM]) Gentzen-type systems or their dual, tableaux, are described as techniques for showing validity of formulae which are more practical than the usual Hilbert-type formalisms. People who have learnt these methods often wonder why the Automated Reasoning community seems to ignore them and prefers instead the resolution method. Some of the classical books on AD (such as CL], Lo]) do not mention these methods at all. Others (such as Ro]) do, but (...)
    Translate
     
     
    Export citation  
     
    Bookmark   6 citations  
  18.  13
    Self-Extensional Three-Valued Paraconsistent Logics.Arnon Avron - 2017 - Logica Universalis 11 (3):297-315.
    A logic \ is called self-extensional if it allows to replace occurrences of a formula by occurrences of an \-equivalent one in the context of claims about logical consequence and logical validity. It is known that no three-valued paraconsistent logic which has an implication can be self-extensional. In this paper we show that in contrast, there is exactly one self-extensional three-valued paraconsistent logic in the language of \ for which \ is a disjunction, and \ is a conjunction. We also (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  19.  63
    Cut-Free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics.Arnon Avron, Jonathan Ben-Naim & Beata Konikowska - 2007 - Logica Universalis 1 (1):41-70.
    . The paper presents a method for transforming a given sound and complete n-sequent proof system into an equivalent sound and complete system of ordinary sequents. The method is applicable to a large, central class of (generalized) finite-valued logics with the language satisfying a certain minimal expressiveness condition. The expressiveness condition decrees that the truth-value of any formula φ must be identifiable by determining whether certain formulas uniformly constructed from φ have designated values or not. The transformation preserves the general (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  20.  55
    A Non-Deterministic View on Non-Classical Negations.Arnon Avron - 2005 - Studia Logica 80 (2-3):159-194.
    We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ+, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics which is (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  21. On Negation, Completeness and Consistency.Arnon Avron - unknown
    We have avoided here the term \false", since we do not want to commit ourselves to the view that A is false precisely when it is not true. Our formulation of the intuition is therefore obviously circular, but this is unavoidable in intuitive informal characterizations of basic connectives and quanti ers.
    Translate
     
     
    Export citation  
     
    Bookmark   5 citations  
  22. Many-Valued Non-Deterministic Semantics for First-Order Logics of Formal (In)Consistency.Arnon Avron - unknown
    A paraconsistent logic is a logic which allows non-trivial inconsistent theories. One of the oldest and best known approaches to the problem of designing useful paraconsistent logics is da Costa’s approach, which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. da Costa’s approach has led to the family of Logics of Formal (In)consistency (LFIs). In this paper we provide non-deterministic semantics for a very large family (...)
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  23.  10
    Four-Valued Paradefinite Logics.Ofer Arieli & Arnon Avron - 2017 - Studia Logica 105 (6):1087-1122.
    Paradefinite logics are logics that can be used for handling contradictory or partial information. As such, paradefinite logics should be both paraconsistent and paracomplete. In this paper we consider the simplest semantic framework for introducing paradefinite logics. It consists of the four-valued matrices that expand the minimal matrix which is characteristic for first degree entailments: Dunn–Belnap matrix. We survey and study the expressive power and proof theory of the most important logics that can be developed in this framework.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  24.  42
    On Modal Systems Having Arithmetical Interpretations.Arnon Avron - 1984 - Journal of Symbolic Logic 49 (3):935-942.
  25. Logical Non-Determinism as a Tool for Logical Modularity: An Introduction.Arnon Avron - unknown
    It is well known that every propositional logic which satisfies certain very natural conditions can be characterized semantically using a multi-valued matrix ([Los and Suszko, 1958; W´ ojcicki, 1988; Urquhart, 2001]). However, there are many important decidable logics whose characteristic matrices necessarily consist of an infinite number of truth values. In such a case it might be quite difficult to find any of these matrices, or to use one when it is found. Even in case a logic does have a (...)
    Translate
     
     
    Export citation  
     
    Bookmark   4 citations  
  26.  49
    Relevant Entailment--Semantics and Formal Systems.Arnon Avron - 1984 - Journal of Symbolic Logic 49 (2):334-342.
  27.  5
    A Paraconsistent View on B and S5.Arnon Avron & Anna Zamansky - 2016 - In Lev Beklemishev, Stéphane Demri & András Máté (eds.), Advances in Modal Logic, Volume 11. CSLI Publications. pp. 21-37.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  28.  6
    Multiplicative Conjunction as an Extensional Conjunction.Arnon Avron - 1997 - Logic Journal of the IGPL 5 (2):181-208.
    We show that the rule that allows the inference of A from A ⊗ B is admissible in many of the basic multiplicative systems. By adding this rule to these systems we get, therefore, conservative extensions in which the tensor behaves as classical conjunction. Among the systems obtained in this way the one derived from RMIm has a particular interest. We show that this system has a simple infinite-valued semantics, relative to which it is strongly complete, and a nice cut-free (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  29.  17
    General Patterns for Nonmonotonic Reasoning: From Basic Entailments to Plausible Relations.O. Arieli & A. Avron - 2000 - Logic Journal of the IGPL 8 (2):119-148.
    This paper has two goals. First, we develop frameworks for logical systems which are able to reflect not only non-monotonic patterns of reasoning, but also paraconsistent reasoning. Our second goal is to have a better understanding of the conditions that a useful relation for nonmonotonic reasoning should satisfy. For this we consider a sequence of generalizations of the pioneering works of Gabbay, Kraus, Lehmann, Magidor and Makinson. These generalizations allow the use of monotonic nonclassical logics as the underlying logic upon (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  30.  52
    Rough Sets and 3-Valued Logics.A. Avron & B. Konikowska - 2008 - Studia Logica 90 (1):69-92.
    In the paper we explore the idea of describing Pawlak’s rough sets using three-valued logic, whereby the value t corresponds to the positive region of a set, the value f — to the negative region, and the undefined value u — to the border of the set. Due to the properties of the above regions in rough set theory, the semantics of the logic is described using a non-deterministic matrix (Nmatrix). With the strong semantics, where only the value t is (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  31.  59
    Whither Relevance Logic?Arnon Avron - 1992 - Journal of Philosophical Logic 21 (3):243 - 281.
  32.  6
    Combining Classical Logic, Paraconsistency and Relevance.Arnon Avron - 2005 - Journal of Applied Logic 3 (1):133-160.
  33.  12
    5-Valued Non-Deterministic Semantics for The Basic Paraconsistent Logic mCi.Arnon Avron - 2008 - Studies in Logic, Grammar and Rhetoric 14 (27).
    One of the most important paraconsistent logics is the logic mCi, which is one of the two basic logics of formal inconsistency. In this paper we present a 5-valued characteristic nondeterministic matrix for mCi. This provides a quite non-trivial example for the utility and effectiveness of the use of non-deterministic many-valued semantics.
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  34.  67
    Relevance and Paraconsistency—a New Approach.Arnon Avron - 1990 - Journal of Symbolic Logic 55 (2):707-732.
  35. A Simple Proof of Completeness and Cut-Elimination for Propositional G¨ Odel Logic.Arnon Avron - unknown
    We provide a constructive, direct, and simple proof of the completeness of the cut-free part of the hypersequential calculus for G¨odel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). We then extend the results and proofs to derivations from assumptions, showing that such derivations can be confined to those in which cuts are made only on formulas which occur in the assumptions.
     
    Export citation  
     
    Bookmark   2 citations  
  36.  7
    Relevance and Paraconsistency-A New Approach Part II: The Formal Systems.Arnon Avron - 1990 - Notre Dame Journal of Formal Logic 31:169-202.
  37.  7
    Quasi-Canonical Systems and Their Semantics.Arnon Avron - forthcoming - Synthese:1-19.
    A canonical Gentzen-type system is a system in which every rule has the subformula property, it introduces exactly one occurrence of a connective, and it imposes no restrictions on the contexts of its applications. A larger class of Gentzen-type systems which is also extensively in use is that of quasi-canonical systems. In such systems a special role is given to a unary connective \ of the language. Accordingly, each application of a logical rule in such systems introduces either a formula (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  38.  36
    Implicational F-Structures and Implicational Relevance Logics.A. Avron - 2000 - Journal of Symbolic Logic 65 (2):788-802.
    We describe a method for obtaining classical logic from intuitionistic logic which does not depend on any proof system, and show that by applying it to the most important implicational relevance logics we get relevance logics with nice semantical and proof-theoretical properties. Semantically all these logics are sound and strongly complete relative to classes of structures in which all elements except one are designated. Proof-theoretically they correspond to cut-free hypersequential Gentzen-type calculi. Another major property of all these logic is that (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  39.  30
    Proof Systems for Reasoning About Computation Errors.Arnon Avron & Beata Konikowska - 2009 - Studia Logica 91 (2):273-293.
    In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  40.  62
    Multi-Valued Semantics: Why and How.Arnon Avron - 2009 - Studia Logica 92 (2):163-182.
    According to Suszko's Thesis,any multi-valued semantics for a logical system can be replaced by an equivalent bivalent one. Moreover: bivalent semantics for families of logics can frequently be developed in a modular way. On the other hand bivalent semantics usually lacks the crucial property of analycity, a property which is guaranteed for the semantics of multi-valued matrices. We show that one can get both modularity and analycity by using the semantic framework of multi-valued non-deterministic matrices. We further show that for (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  41.  7
    Rexpansions of Nondeterministic Matrices and Their Applications in Nonclassical Logics.Arnon Avron & Yoni Zohar - 2019 - Review of Symbolic Logic 12 (1):173-200.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42.  35
    Relevance and Paraconsistency---A New Approach. II. The Formal Systems.Arnon Avron - 1990 - Notre Dame Journal of Formal Logic 31 (2):169-202.
  43.  24
    Decomposition Proof Systems for Gödel-Dummett Logics.Arnon Avron & Beata Konikowska - 2001 - Studia Logica 69 (2):197-219.
    The main goal of the paper is to suggest some analytic proof systems for LC and its finite-valued counterparts which are suitable for proof-search. This goal is achieved through following the general Rasiowa-Sikorski methodology for constructing analytic proof systems for semantically-defined logics. All the systems presented here are terminating, contraction-free, and based on invertible rules, which have a local character and at most two premises.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  44.  24
    Gentzenizing Schroeder-Heister's Natural Extension of Natural Deduction.Arnon Avron - 1989 - Notre Dame Journal of Formal Logic 31 (1):127-135.
  45.  16
    On Purely Relevant Logics.Arnon Avron - 1986 - Notre Dame Journal of Formal Logic 27 (2):180-194.
  46.  30
    Multiplicative Conjunction and an Algebraic Meaning of Contraction and Weakening.A. Avron - 1998 - Journal of Symbolic Logic 63 (3):831-859.
    We show that the elimination rule for the multiplicative (or intensional) conjunction $\wedge$ is admissible in many important multiplicative substructural logics. These include LL m (the multiplicative fragment of Linear Logic) and RMI m (the system obtained from LL m by adding the contraction axiom and its converse, the mingle axiom.) An exception is R m (the intensional fragment of the relevance logic R, which is LL m together with the contraction axiom). Let SLL m and SR m be, respectively, (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  47.  8
    Two Types of Multiple-Conclusion Systems.A. Avron - 1998 - Logic Journal of the IGPL 6 (5):695-718.
    Hypersequents are finite sets of ordinary sequents. We show that multiple-conclusion sequents and single-conclusion hypersequents represent two different natural methods of switching from a single-conclusion calculus to a multiple-conclusion one. The use of multiple-conclusion sequents corresponds to using a multiplicative disjunction, while the use of single-conclusion hypersequents corresponds to using an additive one. Moreover: each of the two methods is usually based on a different natural semantic idea and accordingly leads to a different class of algebraic structures. In the cases (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  48. A Framework for Formalizing Set Theories Based on the Use of Static Set Terms.Arnon Avron - unknown
    We present a new unified framework for formalizations of axiomatic set theories of different strength, from rudimentary set theory to full ZF . It allows the use of set terms, but provides a static check of their validity. Like the inconsistent “ideal calculus” for set theory, it is essentially based on just two set-theoretical principles: extensionality and comprehension (to which we add ∈-induction and optionally the axiom of choice). Comprehension is formulated as: x ∈ {x | ϕ} ↔ ϕ, where (...)
    No categories
     
    Export citation  
     
    Bookmark   1 citation  
  49. Canonical Constructive Systems ⋆.Arnon Avron - unknown
    We define the notions of a canonical inference rule and a canonical system in the framework of single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and prove that such a canonical system is non-trivial iff it is coherent (where coherence is a constructive condition). Next we develop a general non-deterministic Kripke-style semantics for such systems, and show that every constructive canonical system (i.e. coherent canonical single-conclusion system) induces a class of non-deterministic Kripke-style frames for which it is strongly sound and (...)
     
    Export citation  
     
    Bookmark   1 citation  
  50.  3
    A Constructive Analysis of $Mathbf{RM}$.Arnon Avron - 1987 - Journal of Symbolic Logic 52 (4):939-951.
1 — 50 / 84