Search results for 'Proof theory Congresses' (try it on Scholar)

1000+ found
Sort by:
  1. H. Wansing (ed.) (1996). Proof Theory of Modal Logic. Kluwer.score: 116.0
    Proof Theory of Modal Logic is devoted to a thorough study of proof systems for modal logics, that is, logics of necessity, possibility, knowledge, belief, time, computations etc. It contains many new technical results and presentations of novel proof procedures. The volume is of immense importance for the interdisciplinary fields of logic, knowledge representation, and automated deduction.
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. K. Schütte, Justus Diller & G. H. Müller (eds.) (1975). Isilc Proof Theory Symposion: Dedicated to Kurt Schütte on the Occasion of His 65th Birthday: Proceedings of the International Summer Institute and Logic Colloquium, Kiel, 1974. Springer-Verlag.score: 102.0
     
    My bibliography  
     
    Export citation  
  3. A. S. Troelstra (2000). Basic Proof Theory. Cambridge University Press.score: 84.0
    This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  4. Ryo Takemura (2013). Proof Theory for Reasoning with Euler Diagrams: A Logic Translation and Normalization. Studia Logica 101 (1):157-191.score: 84.0
    Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  5. 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.score: 84.0
    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.
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. Samuel R. Buss (ed.) (1998). Handbook of Proof Theory. Elsevier.score: 84.0
    This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  7. Irving H. Anellis (2012). Jean van Heijenoort's Contributions to Proof Theory and Its History. Logica Universalis 6 (3-4):411-458.score: 84.0
    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.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  8. Dov M. Gabbay (2000). Goal-Directed Proof Theory. Kluwer Academic.score: 84.0
    Goal Directed Proof Theory presents a uniform and coherent methodology for automated deduction in non-classical logics, the relevance of which to computer science is now widely acknowledged. The methodology is based on goal-directed provability. It is a generalization of the logic programming style of deduction, and it is particularly favourable for proof search. The methodology is applied for the first time in a uniform way to a wide range of non-classical systems, covering intuitionistic, intermediate, modal and substructural (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. David J. Pym (2004). Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control. Oxford University Press.score: 73.0
    This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search including proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences.
    Direct download  
     
    My bibliography  
     
    Export citation  
  10. Paolo Maffezioli & Alberto Naibo (forthcoming). Proof Theory of Epistemic Logic of Programs. Logic and Logical Philosophy.score: 73.0
    A combination of epistemic logic and dynamic logic of programs is presented. Although rich enough to formalize some simple game-theoretic scenarios, its axiomatization is problematic as it leads to the paradoxical conclusion that agents are omniscient. A cut-free labelled Gentzen-style proof system is then introduced where knowledge and action, as well as their combinations, are formulated as rules of inference, rather than axioms. This provides a logical framework for reasoning about games in a modular and systematic way, and to (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  11. Luciano Serafini & Fausto Giunchiglia (2002). ML Systems: A Proof Theory for Contexts. [REVIEW] Journal of Logic, Language and Information 11 (4):471-518.score: 73.0
    In the last decade the concept of context has been extensivelyexploited in many research areas, e.g., distributed artificialintelligence, multi agent systems, distributed databases, informationintegration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion ofcontext have been proposed: Giunchiglia and Serafini's Multi LanguageSystems (ML systems), McCarthy's modal logics of contexts, andGabbay's Labelled Deductive Systems.Previous papers have argued in favor of ML systems with respect to theother approaches. Our aim in this paper is to support these arguments froma (...)
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  12. Stefano Baratella & Andrea Masini (2004). An Approach to Infinitary Temporal Proof Theory. Archive for Mathematical Logic 43 (8):965-990.score: 73.0
    Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an ω–type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  13. Erik Palmgren (2012). Proof-Relevance of Families of Setoids and Identity in Type Theory. Archive for Mathematical Logic 51 (1-2):35-47.score: 72.0
    Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  14. Carlo Cellucci (1985). Proof Theory and Complexity. Synthese 62 (2):173 - 189.score: 71.0
    Different proofs may be distinguished in terms of complexity. This paper reviews the inefficiency of current logical systems.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  15. Paolo Maffezioli, Alberto Naibo & Sara Negri (2013). The Church–Fitch Knowability Paradox in the Light of Structural Proof Theory. Synthese 190 (14):2677-2716.score: 70.0
    Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$ , by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$ (KP). The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$ (OP). A Gentzen-style reconstruction of the Church–Fitch (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  16. Sören Stenlund (1972). Combinators, -Terms and Proof Theory. Dordrecht,D. Reidel.score: 70.0
    The main aim of Schonfinkel's paper was methodological: to reduce the primitive logical notions to as few and definite notions as possible. ...
    Direct download  
     
    My bibliography  
     
    Export citation  
  17. Gerhard Jäger (1986). Theories for Admissible Sets: A Unifying Approach to Proof Theory. Bibliopolis.score: 70.0
     
    My bibliography  
     
    Export citation  
  18. Bruno Scarpellini (1971). Proof Theory and Intuitionistic Systems. New York,Springer-Verlag.score: 70.0
  19. K. Schütte (1977). Proof Theory. Springer-Verlag.score: 70.0
     
    My bibliography  
     
    Export citation  
  20. David Steiner & Thomas Strahm (2006). On the Proof Theory of Type Two Functionals Based on Primitive Recursive Operations. Mathematical Logic Quarterly 52 (3):237-252.score: 70.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  21. Gaisi Takeuti (1987). Proof Theory. Sole Distributors for the U.S.A. And Canada, Elsevier Science Pub. Co..score: 70.0
     
    My bibliography  
     
    Export citation  
  22. Greg Restall (2009). Truth Values and Proof Theory. Studia Logica 92 (2):241 - 264.score: 62.0
    I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, an idealisation of more fundamental logical features in the proof theory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  23. A. Kino, John Myhill & Richard Eugene Vesley (eds.) (1970). Intuitionism and Proof Theory. Amsterdam,North-Holland Pub. Co..score: 62.0
    Our first aim is to make the study of informal notions of proof plausible. Put differently, since the raison d'étre of anything like existing proof theory seems to rest on such notions, the aim is nothing else but to make a case for proof theory; ...
    Direct download  
     
    My bibliography  
     
    Export citation  
  24. Andrew Arana (2010). Proof Theory in Philosophy of Mathematics. Philosophy Compass 5 (4):336-347.score: 56.0
    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.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  25. Shawn Hedman (2004). A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Oxford University Press.score: 56.0
    The ability to reason and think in a logical manner forms the basis of learning for most mathematics, computer science, philosophy and logic students. Based on the author's teaching notes at the University of Maryland and aimed at a broad audience, this text covers the fundamental topics in classical logic in an extremely clear, thorough and accurate style that is accessible to all the above. Covering propositional logic, first-order logic, and second-order logic, as well as proof theory, computability (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  26. Solomon Feferman, The Proof Theory of Classical and Constructive Inductive Definitions. A 40 Year Saga, 1968-2008.score: 56.0
    1. Pohlers and The Problem. I first met Wolfram Pohlers at a workshop on proof theory organized by Walter Felscher that was held in Tübingen in early April, 1973. Among others at that workshop relevant to the work surveyed here were Kurt Schütte, Wolfram’s teacher in Munich, and Wolfram’s fellow student Wilfried Buchholz. This is not meant to slight in the least the many other fine logicians who participated there.2 In Tübingen I gave a couple of survey (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  27. Gaisi Takeuti (1985). Proof Theory and Set Theory. Synthese 62 (2):255 - 263.score: 56.0
    The foundations of mathematics are divided into proof theory and set theory. Proof theory tries to justify the world of infinite mind from the standpoint of finite mind. Set theory tries to know more and more of the world of the infinite mind. The development of two subjects are discussed including a new proof of the accessibility of ordinal diagrams. Finally the world of large cardinals appears when we go slightly beyond girard's categorical (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  28. Jeremy Avigad, “Clarifying the Nature of the Infinite”: The Development of Metamathematics and Proof Theory.score: 56.0
    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.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  29. Jeremy Avigad, Proof Theory.score: 56.0
    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 (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  30. Jeremy Avigad (2004). Forcing in Proof Theory. Bulletin of Symbolic Logic 10 (3):305-333.score: 56.0
    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 (...)
    Direct download (13 more)  
     
    My bibliography  
     
    Export citation  
  31. Grigori Mints (1991). Proof Theory in the USSR 1925-1969. Journal of Symbolic Logic 56 (2):385-424.score: 56.0
    We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  32. Reinhard Kahle (2002). Mathematical Proof Theory in the Light of Ordinal Analysis. Synthese 133 (1/2):237 - 255.score: 56.0
    We give an overview of recent results in ordinal analysis. Therefore, we discuss the different frameworks used in mathematical proof-theory, namely "subsystem of analysis" including "reverse mathematics", "Kripke-Platek set theory", "explicit mathematics", "theories of inductive definitions", "constructive set theory", and "Martin-Löf's type theory".
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  33. George Tourlakis (2010). On the Proof-Theory of Two Formalisations of Modal First-Order Logic. Studia Logica 96 (3):349-373.score: 56.0
    We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  34. Christian G. Fermüller & George Metcalfe (2009). Giles's Game and the Proof Theory of Łukasiewicz Logic. Studia Logica 92 (1):27 - 61.score: 56.0
    In the 1970s, Robin Giles introduced a game combining Lorenzen-style dialogue rules with a simple scheme for betting on the truth of atomic statements, and showed that the existence of winning strategies for the game corresponds to the validity of formulas in Łukasiewicz logic. In this paper, it is shown that ‘disjunctive strategies’ for Giles’s game, combining ordinary strategies for all instances of the game played on the same formula, may be interpreted as derivations in a corresponding proof system. (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  35. Wilfried Sieg, Proof Theory.score: 56.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  36. Solomon Feferman (2000). Does Reductive Proof Theory Have a Viable Rationale? Erkenntnis 53 (1-2):63-96.score: 56.0
    The goals of reduction andreductionism in the natural sciences are mainly explanatoryin character, while those inmathematics are primarily foundational.In contrast to global reductionistprograms which aim to reduce all ofmathematics to one supposedly ``universal'' system or foundational scheme, reductive proof theory pursues local reductions of one formal system to another which is more justified in some sense. In this direction, two specific rationales have been proposed as aims for reductive proof theory, the constructive consistency-proof rationale and (...)
    Direct download (9 more)  
     
    My bibliography  
     
    Export citation  
  37. Sara Negri & Jan von Plato (2001). Structural Proof Theory. Cambridge University Press.score: 56.0
    A concise introduction to structural proof theory, a branch of logic studying the general structure of logical and mathematical proofs.
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  38. S. Buss (1998). Chapter 1: An Introduction to Proof Theory & Chapter 2: Firstorder Proof Theory of Arithmetic. In Samuel R. Buss (ed.), Handbook of Proof Theory. Elsevier.score: 56.0
    No categories
     
    My bibliography  
     
    Export citation  
  39. Harold Schellinx (1996). A Linear Approach to Modal Proof Theory. In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer. 33.score: 56.0
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  40. Yehuda Schwartz & George Tourlakis (forthcoming). On the Proof-Theory of a First-Order Extension of GL. Logic and Logical Philosophy.score: 56.0
    We introduce a first order extension of GL, called ML 3 , and develop its proof theory via a proxy cut-free sequent calculus GLTS. We prove the highly nontrivial result that cut is a derived rule in GLTS, a result that is unavailable in other known first-order extensions of GL. This leads to proofs of weak reflection and the related conservation result for ML 3 , as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  41. Wilfried Sieg, Church's Thesis, "Consistency", "Formalization", "Proof Theory" : Dictionary Entries.score: 56.0
    Wilfred Sieg. “Church's Thesis”, “Consistency”, “Formalization”, “Proof Theory”: Dictionary Entries.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  42. Wilfried Sieg, Mechanisms and Search: Aspects of Proof Theory.score: 56.0
    Wilfred Sieg. Mechanisms and Search: Aspects of Proof Theory.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  43. David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.score: 54.0
    The II-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the II-calculus and prove the cut-elimination theorem.The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  44. Sara Negri (1999). Sequent Calculus Proof Theory of Intuitionistic Apartness and Order Relations. Archive for Mathematical Logic 38 (8):521-547.score: 54.0
    Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity results for the theories (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  45. Wendy MacCaull (1998). Relational Semantics and a Relational Proof System for Full Lambek Calculus. Journal of Symbolic Logic 63 (2):623-637.score: 51.0
    In this paper we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a list of conditions on the relations. It is accompanied by a Kripke-style (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  46. C. F. M. Vermeulen (2000). Text Structure and Proof Structure. Journal of Logic, Language and Information 9 (3):273-311.score: 51.0
    This paper is concerned with the structure of texts in which aproof is presented. Some parts of such a text are assumptions, otherparts are conclusions. We show how the structural organisation of thetext into assumptions and conclusions helps to check the validity of theproof. Then we go on to use the structural information for theformulation of proof rules, i.e., rules for the (re-)construction ofproof texts. The running example is intuitionistic propositional logicwith connectives , and. We give new proofs of (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  47. Lars Hallnäs (2006). On the Proof-Theoretic Foundation of General Definition Theory. Synthese 148 (3):589 - 602.score: 50.0
    A general definition theory should serve as a foundation for the mathematical study of definitional structures. The central notion of such a theory is a precise explication of the intuitively given notion of a definitional structure. The purpose of this paper is to discuss the proof theory of partial inductive definitions as a foundation for this kind of a more general definition theory. Among the examples discussed is a suggestion for a more abstract definition of (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  48. Manfred Szabo (1970). On the Original Gentzen Consistency Proof for Number Theory. In A. Kino, John Myhill & Richard Eugene Vesley (eds.), Intuitionism and Proof Theory. Amsterdam,North-Holland Pub. Co.. 409.score: 50.0
    No categories
     
    My bibliography  
     
    Export citation  
  49. Sara Negri (2011). Proof Analysis: A Contribution to Hilbert's Last Problem. Cambridge University Press.score: 49.0
    Machine generated contents note: Prologue: Hilbert's Last Problem; 1. Introduction; Part I. Proof Systems Based on Natural Deduction: 2. Rules of proof: natural deduction; 3. Axiomatic systems; 4. Order and lattice theory; 5. Theories with existence axioms; Part II. Proof Systems Based on Sequent Calculus: 6. Rules of proof: sequent calculus; 7. Linear order; Part III. Proof Systems for Geometric Theories: 8. Geometric theories; 9. Classical and intuitionistic axiomatics; 10. Proof analysis in elementary (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  50. Giovanni Sambin & Jan M. Smith (eds.) (1998). Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995. Oxford University Press.score: 49.0
    This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.
    Direct download  
     
    My bibliography  
     
    Export citation  
1 — 50 / 1000