Related categories

2370 found
Order:
1 — 50 / 2370
  1. Proving Theorems of the Second Order Lambek Calculus in Polynomial Time.Erik Aarts - 1994 - Studia Logica 53 (3):373 - 387.
    In the Lambek calculus of order 2 we allow only sequents in which the depth of nesting of implications is limited to 2. We prove that the decision problem of provability in the calculus can be solved in time polynomial in the length of the sequent. A normal form for proofs of second order sequents is defined. It is shown that for every proof there is a normal form proof with the same axioms. With this normal form we can give (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  2. Toward A Visual Proof System: Lewis Carroll's Method of Trees.Francine F. Abeles - 2012 - Logica Universalis 6 (3-4):521-534.
    In the period 1893–1897 Charles Dodgson, writing as Lewis Carroll, published two books and two articles on logic topics. Manuscript material first published in 1977 together with letters and diary entries provide evidence that he was working toward a visual proof system for complex syllogistic propositional logic based on a mechanical tree method that he devised.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  3. KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests.Kamal Aboul-Hosn & Dexter Kozen - 2006 - Journal of Applied Non-Classical Logics 16 (1-2):9-33.
  4. Machine Verification of Mathematical Proof.Paul W. Abrahams - 1972 - Journal of Symbolic Logic 37 (2):411-412.
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
  5. Handbook of Logic in Computer Science.Samson Abramsky, Dov M. Gabbay & Thomas S. E. Maibaum - 1992
    Remove from this list  
     
    Export citation  
     
    My bibliography   6 citations  
  6. Some Proof Theoretical Remarks on Quantification in Ordinary Language.Michele Abrusci & Christian Retoré - manuscript
    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  
  7. Sequent Calculus and Phase Semantics for Pure Non-Commutative Classical Propositional Logic.V. M. Abrusci - 1991 - Journal of Symbolic Logic 56:1403-1451.
    Remove from this list  
     
    Export citation  
     
    My bibliography   2 citations  
  8. On Hilbert's Axiomatics of Propositional Logic.V. Michele Abrusci - 2014 - Perspectives on Science 22 (1):115-132.
    Hilbert's conference lectures during the year 1922, Neuebegründung der Mathematik. Erste Mitteilung and Die logischen Grundlagen der Mathematik (both are published in (Hilbert [1935] 1965) pp. 157-195), contain his first public presentation of an axiom system for propositional logic, or at least for a fragment of propositional logic, which is largely influenced by the study on logical woks of Frege and Russell during the previous years.The year 1922 is at the beginning of Hilbert's foundational program in its definitive form. The (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  9. Phase Semantics and Sequent Calculus for Pure Noncommutative Classical Linear Propositional Logic.V. Michele Abrusci - 1991 - Journal of Symbolic Logic 56 (4):1403-1451.
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography   8 citations  
  10. A Comparison Between Lambek Syntactic Calculus and Intuitionistic Linear Propositional Logic.V. Michele Abrusci - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (1):11-15.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  11. Non-Commutative Intuitionistic Linear Logic.V. Michele Abrusci - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (4):297-318.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  12. A New Correctness Criterion for Cyclic Proof Nets.V. Michele Abrusci & Elena Maringelli - 1998 - Journal of Logic, Language and Information 7 (4):449-459.
    We define proof nets for cyclic multiplicative linear logic as edge bi-coloured graphs. Our characterization is purely graph theoretical and works without further complication for proof nets with cuts, which are usually harder to handle in the non-commutative case. This also provides a new characterization of the proof nets for the Lambek calculus (with the empty sequence) which simply are a restriction on the formulas to be considered (which are asked to be intuitionistic).
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  13. Non-Commutative Logic I: The Multiplicative Fragment.V. Michele Abrusci & Paul Ruet - 1999 - Annals of Pure and Applied Logic 101 (1):29-64.
    We introduce proof nets and sequent calculus for the multiplicative fragment of non-commutative logic, which is an extension of both linear logic and cyclic linear logic. The two main technical novelties are a third switching position for the non-commutative disjunction, and the structure of order variety.
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  14. Curry Haskell B.. The Elimination Theorem When Modality is Present.Wilhelm Ackermann - 1955 - Journal of Symbolic Logic 20 (1):67.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  15. Review: Haskell B. Curry, The Elimination Theorem When Modality is Present. [REVIEW]Wilhelm Ackermann - 1955 - Journal of Symbolic Logic 20 (1):67-67.
  16. Rudimentary and Arithmetical Constructive Set Theory.Peter Aczel - 2013 - Annals of Pure and Applied Logic 164 (4):396-415.
    The aim of this paper is to formulate and study two weak axiom systems for the conceptual framework of constructive set theory . Arithmetical CST is just strong enough to represent the class of von Neumann natural numbers and its arithmetic so as to interpret Heyting Arithmetic. Rudimentary CST is a very weak subsystem that is just strong enough to represent a constructive version of Jensenʼs rudimentary set theoretic functions and their theory. The paper is a contribution to the study (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  17. Proof Theory: A Selection of Papers From the Leeds Proof Theory Programme, 1990.Peter Aczel, Harold Simmons & S. S. Wainer (eds.) - 1992 - 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  
  18. A Note on the E1 Collection Scheme and Fragments of Bounded Arithmetic.Zofia Adamowicz & Leszek Aleksander Kolodziejczyk - 2010 - Mathematical Logic Quarterly 56 (2):126-130.
    We show that for each n ≥ 1, if T2n does not prove the weak pigeonhole principle for Σbn functions, then the collection scheme B Σ1 is not finitely axiomatizable over T2n. The same result holds with Sn2 in place of T 2n.
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  19. A Game-Based Formal System for Ł ${}_{\Infty}$.Alan Adamson & Robin Giles - 1979 - Studia Logica 38 (1):49 - 73.
    A formal system for Ł ${}_{\infty}$ , based on a "game-theoretic" analysis of the Łukasiewicz propositional connectives, is defined and proved to be complete. An "Herbrand theorem" for the Ł ${}_{\infty}$ predicate calculus (a variant of some work of Mostowski) and some corollaries relating to its axiomatizability are proved. The predicate calculus with equality is also considered.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  20. A Gentzen System Equivalent to the BCK-Logic'.R. Adillon & Ventura Verdú - 1996 - Bulletin of the Section of Logic 25 (2):73-79.
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
  21. On a Contraction-Less Intuitionistic Propositional Logic with Conjunction and Fusion.Romà J. Adillon & Ventura Verdú - 2000 - Studia Logica 65 (1):11-30.
    In this paper we prove the equivalence between the Gentzen system G LJ*\c , obtained by deleting the contraction rule from the sequent calculus LJ* (which is a redundant version of LJ), the deductive system IPC*\c and the equational system associated with the variety RL of residuated lattices. This means that the variety RL is the equivalent algebraic semantics for both systems G LJ*\c in the sense of [18] and [4], respectively. The equivalence between G LJ*\c and IPC*\c is a (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  22. Gödel’s Notre Dame Course.Miloš Adžić & Kosta Došen - 2016 - Bulletin of Symbolic Logic 22 (4):469-481.
    This is a companion to a paper by the authors entitled “Gödel’s natural deduction,” which presented and made comments about the natural deduction system in Gödel’s unpublished notes for the elementary logic course he gave at the University of Notre Dame in 1939. In that earlier paper, which was itself a companion to a paper that examined the links between some philosophical views ascribed to Gödel and general proof theory, one can find a brief summary of Gödel’s notes for the (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  23. On the Computational Complexity of Cut-Reduction.Klaus Aehlig & Arnold Beckmann - 2010 - Annals of Pure and Applied Logic 161 (6):711-736.
    Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  24. Classical Logic, Intuitionistic Logic, and the Peirce Rule.Henry Africk - 1992 - 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  
  25. A Proof Theoretic Proof of Scott's General Interpolation Theorem.Henry Africk - 1972 - Journal of Symbolic Logic 37 (4):683-695.
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  26. A Note on the Theory of Positive Induction, {{Rm ID}^*_1}.Bahareh Afshari & Michael Rathjen - 2010 - Archive for Mathematical Logic 49 (2):275-281.
    The article shows a simple way of calibrating the strength of the theory of positive induction, ${{\rm ID}^{*}_{1}}$ . Crucially the proof exploits the equivalence of ${\Sigma^{1}_{1}}$ dependent choice and ω-model reflection for ${\Pi^{1}_{2}}$ formulae over ACA 0. Unbeknown to the authors, D. Probst had already determined the proof-theoretic strength of ${{\rm ID}^{*}_{1}}$ in Probst, J Symb Log, 71, 721–746, 2006.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  27. Reverse Mathematics and Well-Ordering Principles: A Pilot Study.Bahareh Afshari & Michael Rathjen - 2009 - 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   2 citations  
  28. A Gentzen-Style Axiomatization for Basic Predicate Calculus.Mojtaba Aghaei & Mohammad Ardeshir - 2003 - 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  
  29. Gentzen-Style Axiomatizations for Some Conservative Extensions of Basic Propositional Logic.Mojtaba Aghaei & Mohammad Ardeshir - 2001 - 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  
  30. Are Tableaux an Improvement of Truth-Tables? Cut-Free Proofs and Bivalence.M. D. Agostino - 1992 - Journal of Logic, Language, and Information 1 (3):127-139.
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  31. Finiteness in Infinite-Valued Łukasiewicz Logic.Stefano Aguzzoli & Agata Ciabattoni - 2000 - Journal of Logic, Language and Information 9 (1):5-29.
    In this paper we deepen Mundici's analysis on reducibility of the decision problem from infinite-valued ukasiewicz logic to a suitable m-valued ukasiewicz logic m , where m only depends on the length of the formulas to be proved. Using geometrical arguments we find a better upper bound for the least integer m such that a formula is valid in if and only if it is also valid in m. We also reduce the notion of logical consequence in to the same (...)
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  32. Some General Results About Proof Normalization.Marc Aiguier & Delphine Longuet - 2010 - 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  
  33. Quasipolynomial Size Frege Proofs of Frankl’s Theorem on the Trace of Sets.James Aisenberg, Maria Luisa Bonet & Sam Buss - 2016 - Journal of Symbolic Logic 81 (2):687-710.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  34. Subformula Semantics for Strong Negation Systems.Seiki Akama - 1990 - 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  
  35. On the Proof Method for Constructive Falsity.Seiki Akama - 1988 - Mathematical Logic Quarterly 34 (5):385-392.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  36. About Cut Elimination for Logics of Common Knowledge.Luca Alberucci & Gerhard Jäger - 2005 - 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   6 citations  
  37. Functional Dependencies Between Variables.Natasha Alechina - 2000 - Studia Logica 66 (2):273-283.
    We consider a predicate logic Lfd where not all assignments of values to individual variables are possible. Some variables are functionally dependent on other variables. This makes sense if the models of logic are assumed to correspond to databases or states. We show that Lfd is undecidable but has a complete and sound sequent calculus formalisation.
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  38. Generalized Quantification as Substructural Logic.Natasha Alechina & Michiel van Lambalgen - 1996 - 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  
  39. Minimum Propositional Proof Length is NP-Hard to Linearly Approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
    We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  40. Applications of Linear Logic to Computation: An Overview.Vladimir Alexiev - 1994 - Logic Journal of the IGPL 2 (1):77-107.
    This paper gives an overview of existing applications of Linear Logic to issues of computation. Alter a substantial introduction to LL, it discusses the implications of LL to functional programming, logic programming, concurrent and object-oriented programming and some other applications of LL, like semantios of negation in LP, non-monotonic issues in AI planning, etc. Although the overview covers pretty much the state-of-the-art in this area, by necessity many of the works are only mentioned and referenced, but not discussed in any (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  41. A Proof-Search Procedure for Intuitionistic Propositional Logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
    A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  42. Glivenko Classes of Sequents for Propositional Star-Free Likelihood Logic.Romas Alonderis - 2006 - Logic Journal of the IGPL 15 (1):1-19.
    We consider conditions under which sequents are derivable in an intuitionistic sequent calculus of propositional star-free likelihood logic iff they are derivable in a classical counterpart of the calculus. Such conditions are defined for sequents with one formula in the succedent and for sequents with empty succedent.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  43. Domains and Lambda-Calculi.Roberto M. Amadio - 1998 - Cambridge University Press.
    This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way, and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  44. Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics.Martin Amerbauer - 1996 - Studia Logica 57 (2-3):359 - 372.
    We give sound and complete tableau and sequent calculi for the prepositional normal modal logics S4.04, K4B and G 0(these logics are the smallest normal modal logics containing K and the schemata A A, A A and A ( A); A A and AA; A A and ((A A) A) A resp.) with the following properties: the calculi for S4.04 and G 0are cut-free and have the interpolation property, the calculus for K4B contains a restricted version of the cut-rule, the (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  45. Synthetic Tableaux for Lukasiewicz's Calculus L3 Mariusz Urbanski.Logique A. Analyse - 2002 - Logique Et Analyse 45:155.
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  46. Pushing the Search Paths in the Proofs. A Study in Proof Heuristics* Diderik Batens and Dagmar Provijn.Logique A. Analyse - 2001 - Logique Et Analyse 44:113.
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  47. Review: M. I. Semenenko, Properties of Some Sublogics of the Classical and Intuitionistic Propositional Calculi. [REVIEW]Alan Ross Anderson - 1974 - Journal of Symbolic Logic 39 (2):351-352.
  48. Church–Rosser Property of a Simple Reduction for Full First-Order Classical Natural Deduction.Y. Andou - 2003 - Annals of Pure and Applied Logic 119 (1-3):225-237.
    A system of typed terms which corresponds with the classical natural deduction with one conclusion and full logical symbols is defined. Church–Rosser property of the system is proved using an extended method of parallel reduction.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  49. Polytime, Combinatory Logic and Positive Safe Induction.Andrea Cantini - 2002 - Archive for Mathematical Logic 41 (2):169-189.
    We characterize the polynomial time operations as those which are provably total in a first order system, which comprises (untyped) combinatory logic with extensionality, together with positive “safe induction” on the set of binary strings. The formalization of safe induction is inspired by Leivants idea of ramification. We also show how to replace ramification by means of modal logic.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  50. Focussing and Proof Construction.Jean-Marc Andreoli - 2001 - Annals of Pure and Applied Logic 107 (1-3):131-163.
    This paper proposes a synthetic presentation of the proof construction paradigm, which underlies most of the research and development in the so-called “logic programming” area. Two essential aspects of this paradigm are discussed here: true non-determinism and partial information. A new formulation of Focussing, the basic property used to deal with non-determinism in proof construction, is presented. This formulation is then used to introduce a general constraint-based technique capable of dealing with partial information in proof construction. One of the baselines (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    My bibliography   6 citations  
1 — 50 / 2370