Related categories
Siblings:
1822 found
Search inside:
(import / add options)   Order:
1 — 50 / 1822
  1. Erik Aarts (1994). Proving Theorems of the Second Order Lambek Calculus in Polynomial Time. 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 (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  2. Francine F. Abeles (2012). Toward A Visual Proof System: Lewis Carroll's Method of Trees. 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. 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  
  4. V. M. Abrusci (1991). Sequent Calculus and Phase Semantics for Pure Non-Commutative Classical Propositional Logic. Journal of Symbolic Logic 56:1403-1451.
    Remove from this list  
     
    Export citation  
     
    My bibliography   2 citations  
  5. V. Michele Abrusci (2014). On Hilbert's Axiomatics of Propositional Logic. 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  
  6. V. Michele Abrusci (1991). Phase Semantics and Sequent Calculus for Pure Noncommutative Classical Linear Propositional Logic. Journal of Symbolic Logic 56 (4):1403-1451.
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    My bibliography   7 citations  
  7. V. Michele Abrusci (1990). A Comparison Between Lambek Syntactic Calculus and Intuitionistic Linear Propositional Logic. 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  
  8. V. Michele Abrusci (1990). Non-Commutative Intuitionistic Linear Logic. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (4):297-318.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  9. V. Michele Abrusci & Elena Maringelli (1998). A New Correctness Criterion for Cyclic Proof Nets. 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  
  10. V. Michele Abrusci & Paul Ruet (1999). Non-Commutative Logic I: The Multiplicative Fragment. 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   5 citations  
  11. Wilhelm Ackermann (1957). Review: A. A. Zykov, The Spectrum Problem in the Extended Predicate Calculus. [REVIEW] Journal of Symbolic Logic 22 (4):360-360.
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
  12. Wilhelm Ackermann (1955). Curry Haskell B.. The Elimination Theorem When Modality is Present. Journal of Symbolic Logic 20 (1):67.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  13. Wilhelm Ackermann (1955). Review: Haskell B. Curry, The Elimination Theorem When Modality is Present. [REVIEW] Journal of Symbolic Logic 20 (1):67-67.
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
  14. 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  
  15. Alan Adamson & Robin Giles (1979). A Game-Based Formal System for Ł ${}_{\Infty}$. 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  
     
    Export citation  
     
    My bibliography  
  16. Romà J. Adillon & Ventura Verdú (2000). On a Contraction-Less Intuitionistic Propositional Logic with Conjunction and Fusion. 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  
  17. 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  
  18. 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 (6 more)  
     
    Export citation  
     
    My bibliography  
  19. Bahareh Afshari & Michael Rathjen (2010). A Note on the Theory of Positive Induction, {{Rm ID}^*_1}. 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   1 citation  
  20. 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   1 citation  
  21. 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  
  22. 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  
  23. Stefano Aguzzoli & Agata Ciabattoni (2000). Finiteness in Infinite-Valued Łukasiewicz Logic. 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  
  24. 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  
  25. 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  
  26. 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   6 citations  
  27. Natasha Alechina (2000). Functional Dependencies Between Variables. 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  
  28. 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  
  29. Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi (2001). Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. 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   1 citation  
  30. R. Alonderis (2013). A Proof-Search Procedure for Intuitionistic Propositional Logic. 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  
  31. Romas Alonderis (2006). Glivenko Classes of Sequents for Propositional Star-Free Likelihood Logic. 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 (2 more)  
     
    Export citation  
     
    My bibliography  
  32. Roberto M. Amadio (1998). Domains and Lambda-Calculi. 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  
  33. Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. 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  
  34. Alan Ross Anderson (1974). Review: M. I. Semenenko, Properties of Some Sublogics of the Classical and Intuitionistic Propositional Calculi. [REVIEW] Journal of Symbolic Logic 39 (2):351-352.
  35. Alan Ross Anderson (1971). Review: L. L. Maksimova, On Models of the Calculus E. [REVIEW] Journal of Symbolic Logic 36 (3):521-521.
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
  36. J. G. Anderson (1973). Review: V. A. Jankov, On the Extension of the Intuitionist Propositional Calculus to the Classical Calculus, and the Minimal Calculus to the Intuitionist Calculus. [REVIEW] Journal of Symbolic Logic 38 (2):331-332.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  37. Jean-Marc Andreoli (2001). Focussing and Proof Construction. 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  
  38. 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 (4 more)  
     
    Export citation  
     
    My bibliography  
  39. 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  
  40. Peter Andrews (1967). Review: Burton Dreben, Stal Aanderaa, Herbrand Analyzing Functions. [REVIEW] Journal of Symbolic Logic 32 (4):521-521.
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  41. Peter Andrews (1967). Review: Burton Dreben, John Denton, A Supplement to Herbrand. [REVIEW] Journal of Symbolic Logic 32 (4):521-522.
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  42. Peter Andrews (1966). Review: W. V. Quine, A Proof Procedure for Quantification Theory. [REVIEW] Journal of Symbolic Logic 31 (4):657-657.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  43. Peter Andrews (1965). Review: Burton S. Dreben, Solvable Suranyi Subclasses: An Introduction to the Herbrand Theory. [REVIEW] Journal of Symbolic Logic 30 (3):390-391.
    Remove from this list  
     
    Export citation  
     
    My bibliography  
  44. Peter B. Andrews & Chad E. Brown (2006). TPS: A Hybrid Automatic-Interactive System for Developing Proofs. Journal of Applied Logic 4 (4):367-395.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  45. Peter Andrews & W. V. Quine (1966). A Proof Procedure for Quantification Theory. Journal of Symbolic Logic 31 (4):657.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  46. Irving Anellis (1991). Forty Years of “Unnatural‘ Natural Deduction and Quantification: A History of First-Order Systems of Natural Deduction From Gentzen, to Copi. Modern Logic 2:113.
    Remove from this list  
     
    Export citation  
     
    My bibliography   1 citation  
  47. 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  
  48. G. Aldo Antonelli (2001). Review: Solomon Feferman, In the Light of Logic. [REVIEW] Bulletin of Symbolic Logic 7 (2):270-277.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  49. 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  
  50. Toshiyasu Arai (2006). Epsilon Substitution Method for $\Pi _{2}^{0}$ -FIX. Journal of Symbolic Logic 71 (4):1155 - 1188.
    In this paper we formulate epsilon substitution method for a theory $\Pi _{2}^{0}$-FIX for non-monotonic $\Pi _{2}^{0}$ inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].
    Remove from this list   Direct download  
     
    Export citation  
     
    My bibliography  
1 — 50 / 1822