Related categories
Siblings:
593 found
Search inside:
(import / add options)   Order:
1 — 50 / 593
  1. Michele Abrusci & Christian Retoré, Some Proof Theoretical Remarks on Quantification in Ordinary Language.
    This paper surveys the common approach to quantification and generalised quantification in formal linguistics and philosophy of language. We point out how this general setting departs from empirical linguistic data, and give some hints for a different view based on proof theory, which on many aspects gets closer to the language itself. We stress the importance of Hilbert's oper- ator epsilon and tau for, respectively, existential and universal quantifications. Indeed, these operators help a lot to construct semantic representation close to (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  2. Peter Aczel, Harold Simmons & S. S. Wainer (eds.) (1992). Proof Theory: A Selection of Papers From the Leeds Proof Theory Programme, 1990. Cambridge University Press.
    This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
  3. Henry Africk (1992). Classical Logic, Intuitionistic Logic, and the Peirce Rule. Notre Dame Journal of Formal Logic 33 (2):229-235.
    A simple method is provided for translating proofs in Grentzen's LK into proofs in Gentzen's LJ with the Peirce rule adjoined. A consequence is a simpler cut elimination operator for LJ + Peirce that is primitive recursive.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  4. Henry Africk (1972). A Proof Theoretic Proof of Scott's General Interpolation Theorem. Journal of Symbolic Logic 37 (4):683-695.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  5. Bahareh Afshari & Michael Rathjen (2009). Reverse Mathematics and Well-Ordering Principles: A Pilot Study. Annals of Pure and Applied Logic 160 (3):231-237.
    The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  6. Mojtaba Aghaei & Mohammad Ardeshir (2003). A Gentzen-Style Axiomatization for Basic Predicate Calculus. Archive for Mathematical Logic 42 (3):245-259.
    We introduce a Gentzen-style sequent calculus axiomatization for Basic Predicate Calculus. Our new axiomatization is an improvement of the previous axiomatizations, in the sense that it has the subformula property. In this system the cut rule is eliminated.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  7. Mojtaba Aghaei & Mohammad Ardeshir (2001). Gentzen-Style Axiomatizations for Some Conservative Extensions of Basic Propositional Logic. Studia Logica 68 (2):263-285.
    We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  8. Marc Aiguier & Delphine Longuet (2010). Some General Results About Proof Normalization. Logica Universalis 4 (1):1-29.
    In this paper, we provide a general setting under which results of normalization of proof trees such as, for instance, the logicality result in equational reasoning and the cut-elimination property in sequent or natural deduction calculi, can be unified and generalized. This is achieved by giving simple conditions which are sufficient to ensure that such normalization results hold, and which can be automatically checked since they are syntactical. These conditions are based on basic properties of elementary combinations of inference rules (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  9. Seiki Akama (1990). Subformula Semantics for Strong Negation Systems. Journal of Philosophical Logic 19 (2):217 - 226.
    We present a semantics for strong negation systems on the basis of the subformula property of the sequent calculus. The new models, called subformula models, are constructed as a special class of canonical Kripke models for providing the way from the cut-elimination theorem to model-theoretic results. This semantics is more intuitive than the standard Kripke semantics for strong negation systems.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  10. Luca Alberucci & Gerhard Jäger (2005). About Cut Elimination for Logics of Common Knowledge. Annals of Pure and Applied Logic 133 (1):73-99.
    The notions of common knowledge or common belief play an important role in several areas of computer science , in philosophy, game theory, artificial intelligence, psychology and many other fields which deal with the interaction within a group of “agents”, agreement or coordinated actions. In the following we will present several deductive systems for common knowledge above epistemic logics –such as K, T, S4 and S5 –with a fixed number of agents. We focus on structural and proof-theoretic properties of these (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  11. David Albrecht, Frank A. Bäuerle, John N. Crossley & John S. Jeavons (1998). Curry-Howard Terms for Linear Logic. Studia Logica 61 (2):223-235.
    In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry- Howard -style terms for this version of linear logic, 3. extend the notion of substitution of Curry- Howard terms for term variables, 4. define the reduction rules for the Curry- Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  12. Natasha Alechina & Michiel van Lambalgen (1996). Generalized Quantification as Substructural Logic. Journal of Symbolic Logic 61 (3):1006-1044.
    We show how sequent calculi for some generalized quantifiers can be obtained by generalizing the Herbrand approach to ordinary first order proof theory. Typical of the Herbrand approach, as compared to plain sequent calculus, is increased control over relations of dependence between variables. In the case of generalized quantifiers, explicit attention to relations of dependence becomes indispensible for setting up proof systems. It is shown that this can be done by turning variables into structured objects, governed by various types of (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  13. James H. Andrews (2007). An Untyped Higher Order Logic with Y Combinator. Journal of Symbolic Logic 72 (4):1385 - 1404.
    We define a higher order logic which has only a notion of sort rather than a notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory, a proof system which is sound with respect to the model theory, and a cut-elimination proof (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  14. P. B. Andrews (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Kluwer Academic Publishers.
    This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography   7 citations  
  15. Irving H. Anellis (2012). Jean van Heijenoort's Contributions to Proof Theory and Its History. Logica Universalis 6 (3-4):411-458.
    Jean van Heijenoort was best known for his editorial work in the history of mathematical logic. I survey his contributions to model-theoretic proof theory, and in particular to the falsifiability tree method. This work of van Heijenoort’s is not widely known, and much of it remains unpublished. A complete list of van Heijenoort’s unpublished writings on tableaux methods and related work in proof theory is appended.
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  16. Toshiyasu Arai (2011). Quick Cut-Elimination for Strictly Positive Cuts. Annals of Pure and Applied Logic 162 (10):807-815.
    In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  17. Toshiyasu Arai (2002). Review: Wilfried Buchholz, Notation Systems for Infinitary Derivations ; Wilfried Buchholz, Explaining Gentzen's Consistency Proof Within Infinitary Proof Theory ; Sergei Tupailo, Finitary Reductions for Local Predicativity, I: Recursively Regular Ordinals. [REVIEW] Bulletin of Symbolic Logic 8 (3):437-439.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  18. Toshiyasu Arai (2002). Epsilon Substitution Method for Theories of Jump Hierarchies. Archive for Mathematical Logic 41 (2):123-153.
    We formulate epsilon substitution method for theories (H)α0 of absolute jump hierarchies, and give two termination proofs of the H-process: The first proof is an adaption of Mints M, Mints-Tupailo-Buchholz MTB, i.e., based on a cut-elimination of a specially devised infinitary calculus. The second one is an adaption of Ackermann Ack. Each termination proof is based on transfinite induction up to an ordinal θ(α0+ ω)0, which is best possible.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  19. Toshiyasu Arai (1998). Some Results on Cut-Elimination, Provable Well-Orderings, Induction and Reflection. Annals of Pure and Applied Logic 95 (1-3):93-184.
    We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  20. Andrew Arana (2010). Proof Theory in Philosophy of Mathematics. Philosophy Compass 5 (4):336-347.
    A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  21. Andrew Arana (2009). On Formally Measuring and Eliminating Extraneous Notions in Proofs. Philosophia Mathematica 17 (2):208–219.
    Many mathematicians and philosophers of mathematics believe some proofs contain elements extraneous to what is being proved. In this paper I discuss extraneousness generally, and then consider a specific proposal for measuring extraneousness syntactically. This specific proposal uses Gentzen’s cut-elimination theorem. I argue that the proposal fails, and that we should be skeptical about the usefulness of syntactic extraneousness measures.
    Remove from this list   Direct download (12 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  22. S. Artemov, B. Kushner, G. Mints, E. Nogina & A. Troelstra (1999). In Memoriam: Albert G. Dragalin, 1941-1998. Bulletin of Symbolic Logic 5 (3):389-391.
  23. Jeremy Avigad, Algebraic Proofs of Cut Elimination.
    Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed as special (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  24. Jeremy Avigad, “Clarifying the Nature of the Infinite”: The Development of Metamathematics and Proof Theory.
    We discuss the development of metamathematics in the Hilbert school, and Hilbert’s proof-theoretic program in particular. We place this program in a broader historical and philosophical context, especially with respect to nineteenth century developments in mathematics and logic. Finally, we show how these considerations help frame our understanding of metamathematics and proof theory today.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  25. Jeremy Avigad, Proof Theory.
    At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in emphasis away (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  26. Jeremy Avigad (2010). Proof Theory. Gödel and the Metamathematical Tradition. In Kurt Gödel, Solomon Feferman, Charles Parsons & Stephen G. Simpson (eds.), Kurt Gödel: Essays for His Centennial. Association for Symbolic Logic
  27. Jeremy Avigad, The Computational Content of Classical Arithmetic to Appear in a Festschrift for Grigori Mints.
    Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various methods of extracting computational information from proofs in classical first-order arithmetic, and reflects on some of the relationships between them. Variants of the Godel-Gentzen double-negation translation, some not so well known, serve to provide canonical and efficient computational interpretations of that theory.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  28. Jeremy Avigad (2004). Forcing in Proof Theory. Bulletin of Symbolic Logic 10 (3):305-333.
    Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...)
    Remove from this list   Direct download (13 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  29. Jeremy Avigad (2002). A Realizability Interpretation for Classical Arithmetic. Bulletin of Symbolic Logic 8 (3):439-440.
    Summary. A constructive realizablity interpretation for classical arithmetic is presented, enabling one to extract witnessing terms from proofs of 1 sentences. The interpretation is shown to coincide with modified realizability, under a novel translation of classical logic to intuitionistic logic, followed by the Friedman-Dragalin translation. On the other hand, a natural set of reductions for classical arithmetic is shown to be compatible with the normalization of the realizing term, implying that certain strategies for eliminating cuts and extracting a witness from (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  30. Jeremy Avigad (2001). Review: Toshiyasu Arai, Some Results on Cut-Elimination, Provable Well-Orderings, Induction and Reflection. [REVIEW] Bulletin of Symbolic Logic 7 (1):77-78.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  31. Jeremy Avigad & Richard Sommer (1997). A Model-Theoretic Approach to Ordinal Analysis. Bulletin of Symbolic Logic 3 (1):17-52.
    We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of numbers with combinatorial properties that, in nonstandard instances, give rise to models of the theory being analyzed. This method is applied to obtain ordinal analyses of a number of interesting subsystems of first- and second-order arithmetic.
    Remove from this list   Direct download (9 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  32. Jeremy Avigad & Richard Zach, The Epsilon Calculus. Stanford Encyclopedia of Philosophy.
    The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term..
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography   3 citations  
  33. A. Avron (1998). Multiplicative Conjunction and an Algebraic Meaning of Contraction and Weakening. 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, (...)
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  34. A. Avron (1998). Formulas for Which Contraction is Admissible. Logic Journal of the Igpl 6 (1):43-48.
    A formula A is said to have the contraction property in a logic L if whenever A, A, Γ ⊨ L B also A, Γ & ; L B. In MLL and in MALL without the additive constants a formula has the contraction property if it is a theorem. Adding the mix rule does not change this fact. In MALL and in affine logic A has the contraction property if either A is provable of A is equivalent to the additive (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
  35. Arnon Avron, Tonk- A Full Mathematical Solution.
    There is a long tradition (See e.g. [9, 10]) starting from [12], according to which the meaning of a connective is determined by the introduction and elimination rules which are associated with it. The supporters of this thesis usually have in mind natural deduction systems of a certain ideal type (explained in Section 3 below). Unfortunately, already the handling of classical negation requires rules which are not of that type. This problem can be solved in the framework of multiple-conclusion Gentzen-type (...)
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  36. Arnon Avron, Gentzen-Type Systems, Resolution and Tableaux.
    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 (...)
    Remove from this list  
    Translate
     
     
    Export citation  
     
    My bibliography   1 citation  
  37. Arnon Avron, The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics.
    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 (...)
    Remove from this list  
     
    Export citation  
     
    My bibliography   3 citations  
  38. Arnon Avron, A Simple Proof of Completeness and Cut-Elimination for Propositional G¨ Odel Logic.
    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.
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  39. Arnon Avron, Canonical Constructive Systems ⋆.
    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 (...)
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  40. Arnon Avron, Canonical Calculi with (N,K)-Ary Quantifiers.
    Propositional canonical Gentzen-type systems, introduced in [2], are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a connective is introduced and no other connective is mentioned. [2] provides a constructive coherence criterion for the non-triviality of such systems and shows that a system of this kind admits cut-elimination iff it is coherent. The semantics of such systems is provided using two-valued non-deterministic matrices (2Nmatrices). [23] extends these results (...)
    Remove from this list  
     
    Export citation  
     
    My bibliography   1 citation  
  41. Arnon Avron, Strong Cut-Elimination, Coherence, and Non-Deterministic Semantics.
    An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence (...)
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  42. Arnon Avron, Simple Consequence Relations.
    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 (...)
    Remove from this list  
     
    Export citation  
     
    My bibliography   12 citations  
  43. Arnon Avron (2014). Paraconsistency, Paracompleteness, Gentzen Systems, and Trivalent Semantics. 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 (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  44. Arnon Avron (1991). A Note of Provability, Truth and Existence. Journal of Philosophical Logic 20 (4):403 - 409.
  45. Arnon Avron (1991). Natural 3-Valued Logics--Characterization and Proof Theory. Journal of Symbolic Logic 56 (1):276-294.
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    My bibliography   23 citations  
  46. Arnon Avron (1990). Relevance and Paraconsistency---A New Approach. II. The Formal Systems. Notre Dame Journal of Formal Logic 31 (2):169-202.
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  47. Arnon Avron (1990). Relevance and Paraconsistency---A New Approach. II. The Formal Systems. Notre Dame Journal of Formal Logic 31 (2):169-202.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  48. Arnon Avron (1989). Gentzenizing Schroeder-Heister's Natural Extension of Natural Deduction. Notre Dame Journal of Formal Logic 31 (1):127-135.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  49. Arnon Avron (1988). The Semantics and Proof Theory of Linear Logic. 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 (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography   23 citations  
  50. Arnon Avron, Jonathan Ben-Naim & Beata Konikowska (2007). Cut-Free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics. 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 (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
1 — 50 / 593