Switch to: References

Citations of:

The formulæ-as-types notion of construction

In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia (1995)

Add citations

You must login to add citations.
  1. What Types Should Not Be.Bruno Bentzen - 2020 - Philosophia Mathematica 28 (1):60-76.
    In a series of papers Ladyman and Presnell raise an interesting challenge of providing a pre-mathematical justification for homotopy type theory. In response, they propose what they claim to be an informal semantics for homotopy type theory where types and terms are regarded as mathematical concepts. The aim of this paper is to raise some issues which need to be resolved for the successful development of their types-as-concepts interpretation.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • (1 other version)Dag Prawitz on Proofs and Meaning.Heinrich Wansing (ed.) - 2014 - Cham, Switzerland: Springer.
    This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Strong Normalization via Natural Ordinal.Daniel Durante Pereira Alves - 1999 - Dissertation,
    The main objective of this PhD Thesis is to present a method of obtaining strong normalization via natural ordinal, which is applicable to natural deduction systems and typed lambda calculus. The method includes (a) the definition of a numerical assignment that associates each derivation (or lambda term) to a natural number and (b) the proof that this assignment decreases with reductions of maximal formulas (or redex). Besides, because the numerical assignment used coincide with the length of a specific sequence of (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Automated reasoning in higher-order logic using the tptp thf infrastructure.Sutcliffe Geoff & Benzmüller Christoph - 2010 - Journal of Formalized Reasoning 3 (1):1-27.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - 2016 - British Journal for the Philosophy of Science:axw006.
    Homotopy Type Theory is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be (...)
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • La priorité de la preuve : le cas de la signification non-standard des constantes logiques.Pascal Boldini - 2004 - Revue Internationale de Philosophie 4:437-447.
    Download  
     
    Export citation  
     
    Bookmark  
  • Fondements ou constructivité ?Mathieu Marion - 2004 - Philosophiques 31 (1):225-230.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The epistemic significance of valid inference.Dag Prawitz - 2012 - Synthese 187 (3):887-898.
    The traditional picture of logic takes it for granted that "valid arguments have a fundamental epistemic significance", but neither model theory nor traditional proof theory dealing with formal system has been able to give an account of this significance. Since valid arguments as usually understood do not in general have any epistemic significance, the problem is to explain how and why we can nevertheless use them sometimes to acquire knowledge. It is suggested that we should distinguish between arguments and acts (...)
    Download  
     
    Export citation  
     
    Bookmark   30 citations  
  • William Tait. The provenance of pure reason. Essays on the philosophy of mathematics and on its history.Charles Parsons - 2009 - Philosophia Mathematica 17 (2):220-247.
    William Tait's standing in the philosophy of mathematics hardly needs to be argued for; for this reason the appearance of this collection is especially welcome. As noted in his Preface, the essays in this book ‘span the years 1981–2002’. The years given are evidently those of publication. One essay was not previously published in its present form, but it is a reworking of papers published during that period. The Introduction, one appendix, and some notes are new. Many of the essays (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • On the unusual effectiveness of logic in computer science.Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi & Victor Vianu - 2001 - Bulletin of Symbolic Logic 7 (2):213-236.
    In 1960, E. P. Wigner, a joint winner of the 1963 Nobel Prize for Physics, published a paper titled On the Unreasonable Effectiveness of Mathematics in the Natural Sciences [61]. This paper can be construed as an examination and affirmation of Galileo's tenet that “The book of nature is written in the language of mathematics”. To this effect, Wigner presented a large number of examples that demonstrate the effectiveness of mathematics in accurately describing physical phenomena. Wigner viewed these examples as (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • A new deconstructive logic: Linear logic.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1997 - Journal of Symbolic Logic 62 (3):755-807.
    The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic using (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Types as graphs: Continuations in type logical grammar. [REVIEW]Chris Barker & Chung-Chieh Shan - 2006 - Journal of Logic, Language and Information 15 (4):331-370.
    Using the programming-language concept of continuations, we propose a new, multimodal analysis of quantification in Type Logical Grammar. Our approach provides a geometric view of in-situ quantification in terms of graphs, and motivates the limited use of empty antecedents in derivations. Just as continuations are the tool of choice for reasoning about evaluation order and side effects in programming languages, our system provides a principled, type-logical way to model evaluation order and side effects in natural language. We illustrate with an (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Relational nouns, pronouns, and resumption.Ash Asudeh - 2005 - Linguistics and Philosophy 28 (4):375 - 446.
    This paper presents a variable-free analysis of relational nouns in Glue Semantics, within a Lexical Functional Grammar (LFG) architecture. Relational nouns and resumptive pronouns are bound using the usual binding mechanisms of LFG. Special attention is paid to the bound readings of relational nouns, how these interact with genitives and obliques, and their behaviour with respect to scope, crossover and reconstruction. I consider a puzzle that arises regarding relational nouns and resumptive pronouns, given that relational nouns can have bound readings (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Constructivity and Computability in Historical and Philosophical Perspective.Jacques Dubucs & Michel Bourdeau (eds.) - 2014 - Dordrecht, Netherland: Springer.
    Ranging from Alan Turing’s seminal 1936 paper to the latest work on Kolmogorov complexity and linear logic, this comprehensive new work clarifies the relationship between computability on the one hand and constructivity on the other. The authors argue that even though constructivists have largely shed Brouwer’s solipsistic attitude to logic, there remain points of disagreement to this day. Focusing on the growing pains computability experienced as it was forced to address the demands of rapidly expanding applications, the content maps the (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The seven virtues of simple type theory.William M. Farmer - 2008 - Journal of Applied Logic 6 (3):267-286.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory.Michael Rathjen - 2005 - Synthese 147 (1):81-120.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Adding logic to the toolbox of molecular biology.Giovanni Boniolo, Marcello D’Agostino, Mario Piazza & Gabriele Pulcini - 2015 - European Journal for Philosophy of Science 5 (3):399-417.
    The aim of this paper is to argue that logic can play an important role in the “toolbox” of molecular biology. We show how biochemical pathways, i.e., transitions from a molecular aggregate to another molecular aggregate, can be viewed as deductive processes. In particular, our logical approach to molecular biology — developed in the form of a natural deduction system — is centered on the notion of Curry-Howard isomorphism, a cornerstone in nineteenth-century proof-theory.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Intuitionistic completeness of first-order logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.
    We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Predicative functionals and an interpretation of ⌢ID.Jeremy Avigad - 1998 - Annals of Pure and Applied Logic 92 (1):1-34.
    In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Gödel's T to theories Pn of “predicative” functionals, which are defined using Martin-Löf's universes of transfinite types. We then extend Gödel's interpretation to the theories of arithmetic inductive definitions IDn, so that each IDn is interpreted in the corresponding Pn. Since the strengths of the theories IDn are cofinal in the ordinal Γ0, as (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • (1 other version)Poincaré et la théorie de la connaissance.Éric Audureau - 2004 - Philosophiques 31 (1):57-88.
    Résumé Partant du principe que la philosophie de la connaissance de Poincaré est cohérente, j’essaie de faire voir que son conventionnalisme en géométrie et en physique n’est qu’une conséquence de son intuitionnisme. Après avoir rappelé, dans la première section, ce qu’est l’intuitionnisme et décrit ce que l’intuitionnisme de Poincaré a de spécifique, je montre, dans la deuxième section, comment celui-ci retentit sur la conception de l’espace. Dans la troisième section, j’applique les conclusions précédemment établies à la question très controversée de (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Formal semantics in modern type theories with coercive subtyping.Zhaohui Luo - 2012 - Linguistics and Philosophy 35 (6):491-513.
    In the formal semantics based on modern type theories, common nouns are interpreted as types, rather than as predicates of entities as in Montague’s semantics. This brings about important advantages in linguistic interpretations but also leads to a limitation of expressive power because there are fewer operations on types as compared with those on predicates. The theory of coercive subtyping adequately extends the modern type theories and, as shown in this paper, plays a very useful role in making type theories (...)
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
  • The Development of Categorical Logic.John L. Bell - unknown
    5.5. Every topos is linguistic: the equivalence theorem.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • (1 other version)Constructive mathematics in theory and programming practice.Douglas Bridges & Steeve Reeves - 1999 - Philosophia Mathematica 7 (1):65-104.
    The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach.Ivo Pezlar - 2017 - Logic and Logical Philosophy 26 (4):473-508.
    In this paper we examine two approaches to the formal treatment of the notion of problem in the paradigm of algorithmic semantics. Namely, we will explore an approach based on Martin-Löf’s Constructive Type Theory, which can be seen as a direct continuation of Kolmogorov’s original calculus of problems, and an approach utilizing Tichý’s Transparent Intensional Logic, which can be viewed as a non-constructive attempt of interpreting Kolmogorov’s logic of problems. In the last section we propose Kolmogorov and CTT-inspired modifications to (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • A Vindication of Program Verification.Selmer Bringsjord - 2015 - History and Philosophy of Logic 36 (3):262-277.
    Fetzer famously claims that program verification is not even a theoretical possibility, and offers a certain argument for this far-reaching claim. Unfortunately for Fetzer, and like-minded thinkers, this position-argument pair, while based on a seminal insight that program verification, despite its Platonic proof-theoretic airs, is plagued by the inevitable unreliability of messy, real-world causation, is demonstrably self-refuting. As I soon show, Fetzer is like the person who claims: ‘My sole claim is that every claim expressed by an English sentence and (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Reasoning about knowledge in linear logic: modalities and complexity.Mathieu Marion & Mehrnouche Sadrzadeh - 2004 - In S. Rahman (ed.), Logic, Epistemology, and the Unity of Science. Dordrecht: Kluwer Academic Publishers. pp. 327--350.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
    The lambdaPi-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 lambdaPi-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 considered (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Choice principles and constructive logics.David Dedivi - 2004 - Philosophia Mathematica 12 (3):222-243.
    to constructive systems is significant for contemporary metaphysics. However, many are surprised by these results, having learned that the Axiom of Choice (AC) is constructively valid. Indeed, even among specialists there were, until recently, reasons for puzzlement-rival versions of Intuitionistic Type Theory, one where (AC) is valid, another where it implies classical logic. This paper accessibly explains the situation, puts the issues in a broader setting by considering other choice principles, and draws philosophical morals for the understanding of quantification, choice (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • The Seeming Interdependence Between the Concepts of Valid Inference and Proof.Dag Prawitz - 2019 - Topoi 38 (3):493-503.
    We may try to explain proofs as chains of valid inference, but the concept of validity needed in such an explanation cannot be the traditional one. For an inference to be legitimate in a proof it must have sufficient epistemic power, so that the proof really justifies its final conclusion. However, the epistemic concepts used to account for this power are in their turn usually explained in terms of the concept of proof. To get out of this circle we may (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • What is a Higher Level Set?Dimitris Tsementzis - 2016 - Philosophia Mathematica:nkw032.
    Structuralist foundations of mathematics aim for an ‘invariant’ conception of mathematics. But what should be their basic objects? Two leading answers emerge: higher groupoids or higher categories. I argue in favor of the former over the latter. First, I explain why to choose between them we need to ask the question of what is the correct ‘categorified’ version of a set. Second, I argue in favor of groupoids over categories as ‘categorified’ sets by introducing a pre-formal understanding of groupoids as (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Kripke-style models for typed lambda calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
    Mitchell, J.C. and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic 51 99–124. The semantics of typed lambda calculus is usually described using Henkin models, consisting of functions over some collection of sets, or concrete cartesian closed categories, which are essentially equivalent. We describe a more general class of Kripke-style models. In categorical terms, our Kripke lambda models are cartesian closed subcategories of the presheaves over a poset. To those familiar with Kripke models of (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Reduction of finite and infinite derivations.G. Mints - 2000 - Annals of Pure and Applied Logic 104 (1-3):167-188.
    We present a general schema of easy normalization proofs for finite systems S like first-order arithmetic or subsystems of analysis, which have good infinitary counterparts S ∞ . We consider a new system S ∞ + with essentially the same rules as S ∞ but different derivable objects: a derivation d∈S ∞ + of a sequent Γ contains a derivation Φ∈S of Γ . Three simple conditions on Φ including a normal form theorem for S ∞ + easily imply a (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Antirealism and the Roles of Truth.B. G. Sundholm - unknown
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • (1 other version)On the proof theory of Coquand's calculus of constructions.Jonathan P. Seldin - 1997 - Annals of Pure and Applied Logic 83 (1):23-101.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Communicative Intentions and Conversational Processes in Human-Human and Human-Computer Dialogue.Matthew Stone - unknown
    This chapter investigates the computational consequences of a broadly Gricean view of language use as intentional activity. In this view, dialogue rests on coordinated reasoning about communicative intentions. The speaker produces each utterance by formulating a suitable communicative intention. The hearer understands it by recognizing the communicative intention behind it. When this coordination is successful, interlocutors succeed in considering the same intentions— that is, the same representations of utterance meaning—as the dialogue proceeds. In this paper, I emphasize that these intentions (...)
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
    We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Constructions, proofs and the meaning of logical constants.Göran Sundholm - 1983 - Journal of Philosophical Logic 12 (2):151 - 172.
    Download  
     
    Export citation  
     
    Bookmark   56 citations  
  • On the adequacy of representing higher order intuitionistic logic as a pure type system.Hans Tonino & Ken-Etsu Fujita - 1992 - Annals of Pure and Applied Logic 57 (3):251-276.
    In this paper we describe the Curry-Howard-De Bruijn isomorphism between Higher Order Many Sorted Intuitionistic Predicate Logic PREDω and the type system λPREDω, which can be considered a subsystem of the Calculus of Constructions. The type system is presented using the concept of a Pure Type System, which is a very elegant framework for describing type systems. We show in great detail how formulae and proof trees of the logic relate to types and terms of the type system, respectively. Finally, (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • The completeness of Heyting first-order logic.W. W. Tait - 2003 - Journal of Symbolic Logic 68 (3):751-763.
    Restricted to first-order formulas, the rules of inference in the Curry-Howard type theory are equivalent to those of first-order predicate logic as formalized by Heyting, with one exception: ∃-elimination in the Curry-Howard theory, where ∃x : A.F (x) is understood as disjoint union, are the projections, and these do not preserve firstorderedness. This note shows, however, that the Curry-Howard theory is conservative over Heyting’s system.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels.James Lipton & Michael J. O'Donnell - 1996 - Annals of Pure and Applied Logic 81 (1-3):187-239.
    We use formal semantic analysis based on new constructions to study abstract realizability, introduced by Läuchli in 1970, and expose its algebraic content. We claim realizability so conceived generates semantics-based intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive reasoning.Well-known semantic formalisms have been defined by Kripke and Beth, but these have no formal concepts corresponding to constructions, and shed little intuitive light on the meanings of formulae. In particular, the completeness proofs for these semantics (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Grammar induction by unification of type-logical lexicons.Sean A. Fulop - 2010 - Journal of Logic, Language and Information 19 (3):353-381.
    A method is described for inducing a type-logical grammar from a sample of bare sentence trees which are annotated by lambda terms, called term-labelled trees . Any type logic from a permitted class of multimodal logics may be specified for use with the procedure, which induces the lexicon of the grammar including the grammatical categories. A first stage of semantic bootstrapping is performed, which induces a general form lexicon from the sample of term-labelled trees using Fulop’s (J Log Lang Inf (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Proof-theoretic Semantics for Classical Mathematics.William W. Tait - 2006 - Synthese 148 (3):603-622.
    We discuss the semantical categories of base and object implicit in the Curry-Howard theory of types and we derive derive logic and, in particular, the comprehension principle in the classical version of the theory. Two results that apply to both the classical and the constructive theory are discussed. First, compositional semantics for the theory does not demand ‘incomplete objects’ in the sense of Frege: bound variables are in principle eliminable. Secondly, the relation of extensional equality for each type is definable (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Implicit epistemic aspects of constructive logic.Göran Sundholm - 1997 - Journal of Logic, Language and Information 6 (2):191-212.
    In the present paper I wish to regard constructivelogic as a self-contained system for the treatment ofepistemological issues; the explanations of theconstructivist logical notions are cast in anepistemological mold already from the outset. Thediscussion offered here intends to make explicit thisimplicit epistemic character of constructivism.Particular attention will be given to the intendedinterpretation laid down by Heyting. This interpretation, especially as refined in the type-theoretical work of Per Martin-Löf, puts thesystem on par with the early efforts of Frege andWhitehead-Russell. This quite (...)
    Download  
     
    Export citation  
     
    Bookmark   32 citations  
  • Term-labeled categorial type systems.Richard T. Oehrle - 1994 - Linguistics and Philosophy 17 (6):633 - 678.
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
  • A correspondence between Martin-löf type theory, the ramified theory of types and pure type systems.Fairouz Kamareddine & Twan Laan - 2001 - Journal of Logic, Language and Information 10 (3):375-402.
    In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, predicative (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • An interpretation of classical proofs.Glen Helman - 1983 - Journal of Philosophical Logic 12 (1):39 - 71.
    Download  
     
    Export citation  
     
    Bookmark  
  • Analytic and synthetic in logic.V. Michele Abrusci - 2016 - Logic Journal of the IGPL 24 (4):481-493.
    Download  
     
    Export citation  
     
    Bookmark  
  • On Modal Logics of Partial Recursive Functions.Pavel Naumov - 2005 - Studia Logica 81 (3):295-309.
    The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Towards mkm in the large: Modular representation and scalable software architecture.Michael Kohlhase - unknown
    MKM has been defined as the quest for technologies to manage mathematical knowledge. MKM “in the small” is well-studied, so the real problem is to scale up to large, highly interconnected corpora: “MKM in the large”. We contend that advances in two areas are needed to reach this goal. We need representation languages that support incremental processing of all primitive MKM operations, and we need software architectures and implementations that implement these operations scalably on large knowledge bases. We present instances (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Dag Prawitz on Proofs, Operations and Grounding.Antonio Piccolomini D’ Aragona - 2019 - Topoi 38 (3):531-550.
    Dag Prawitz’s theory of grounds proposes a fresh approach to valid inferences. Its main aim is to clarify nature and reasons of their epistemic power. The notion of ground is taken to denote what one is in possession of when in a state of evidence, and valid inferences are described in terms of operations that make us pass from grounds we already have to new grounds. Thanks to a rigorously developed proof-as-chains conception, the ground-theoretic framework permits Prawitz to overcome some (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations