Results for 'Cirquent calculus'

941 found
Order:
  1.  23
    Elementary-base cirquent calculus II: Choice quantifiers.Giorgi Japaridze - forthcoming - Logic Journal of the IGPL.
    Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article ‘Elementary-base cirquent calculus I: Parallel and choice connectives’ built the sound and complete axiomatization $\textbf{CL16}$ of a propositional fragment of computability logic. The atoms of the language of $\textbf{CL16}$ represent elementary, i.e. moveless, games and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version $\textbf{CL17}$ of $\textbf{CL16}$, also enjoying soundness and (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2.  7
    A Propositional Cirquent Calculus for Computability Logic.Giorgi Japaridze - 2024 - Journal of Logic, Language and Information 33 (4):363-389.
    Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization  CL18 \text{ CL18 } CL18 of the basic propositional fragment of computability logic—the game-semantically conceived logic of computational resources and tasks. The nonlogical atoms of this fragment represent arbitrary so called static games, and the connectives of its logical vocabulary are negation and the parallel and choice versions of conjunction and disjunction. The main technical (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  3.  31
    A cirquent calculus system with clustering and ranking.Wenyan Xu - 2016 - Journal of Applied Logic 16:37-49.
  4.  40
    The taming of recurrences in computability logic through cirquent calculus, Part I.Giorgi Japaridze - 2013 - Archive for Mathematical Logic 52 (1-2):173-212.
    This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation ${\neg}$ , parallel conjunction ${\wedge}$ , parallel disjunction ${\vee}$ , branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  72
    The taming of recurrences in computability logic through cirquent calculus, Part II.Giorgi Japaridze - 2013 - Archive for Mathematical Logic 52 (1-2):213-259.
    This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}¬{{\neg}}\end{document}, parallel conjunction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}{{\wedge}}\end{document}, parallel disjunction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}{{\vee}}\end{document}, branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  57
    The Parallel versus Branching Recurrences in Computability Logic.Wenyan Xu & Sanyang Liu - 2013 - Notre Dame Journal of Formal Logic 54 (1):61-78.
    This paper shows that the basic logic induced by the parallel recurrence $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ of computability logic (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}},\hspace {-2pt}\mbox {\raisebox {0.12cm}{\@setfontsize \small {7}{8}$\vee$}\hspace {-3.6pt}\raisebox {0.02cm}{\tiny $\mid$}\hspace {2pt}}\}$ ) is a proper superset of the basic logic induced by the branching recurrence $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7. jaskowskps matrix criterion for the iNTurnoNisnc.Proposmonal Calculus - 1973 - In Stanisław J. Surma, Studies in the history of mathematical logic. Wrocław,: Zakład Narodowy im. Ossolinskich. pp. 87.
    No categories
     
    Export citation  
     
    Bookmark  
  8. (1 other version)The identity of individuals in a strict functional calculus of second order.Ruth C. Barcan - 1947 - Journal of Symbolic Logic 12 (1):12-15.
  9. The first computational theory of mind and brain: A close look at McCulloch and Pitts' Logical Calculus of Ideas Immanent in Nervous Activity.Gualtiero Piccinini - 2004 - Synthese 141 (2):175-215.
    Despite its significance in neuroscience and computation, McCulloch and Pitts's celebrated 1943 paper has received little historical and philosophical attention. In 1943 there already existed a lively community of biophysicists doing mathematical work on neural networks. What was novel in McCulloch and Pitts's paper was their use of logic and computation to understand neural, and thus mental, activity. McCulloch and Pitts's contributions included (i) a formalism whose refinement and generalization led to the notion of finite automata (an important formalism in (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   38 citations  
  10.  63
    Notes on the axiomatics of the propositional calculus.C. A. Meredith & A. N. Prior - 1963 - Notre Dame Journal of Formal Logic 4 (3):171-187.
  11.  61
    Spatial logic of tangled closure operators and modal mu-calculus.Robert Goldblatt & Ian Hodkinson - 2017 - Annals of Pure and Applied Logic 168 (5):1032-1090.
  12. The deduction theorem in a functional calculus of first order based on strict implication.Ruth C. Barcan - 1946 - Journal of Symbolic Logic 11 (4):115-118.
  13.  36
    Nowhere to run, rabbit: the cold-war calculus of disease ecology.Warwick Anderson - 2017 - History and Philosophy of the Life Sciences 39 (2):13.
    During the cold war, Frank Fenner and Francis Ratcliffe studied mathematically the coevolution of host resistance and parasite virulence when myxomatosis was unleashed on Australia’s rabbit population. Later, Robert May called Fenner the “real hero” of disease ecology for his mathematical modeling of the epidemic. While Ratcliffe came from a tradition of animal ecology, Fenner developed an ecological orientation in World War II through his work on malaria control —that is, through studies of tropical medicine. This makes Fenner at least (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  14.  12
    The History of the Calculus and Its Conceptual Development: (The Concepts of the Calculus).Carl B. Boyer - 1949 - Courier Corporation.
    Traces the development of the integral and the differential calculus and related theories since ancient times.
    Direct download  
     
    Export citation  
     
    Bookmark   57 citations  
  15.  33
    (1 other version)A comparison between lambek syntactic calculus and intuitionistic linear propositional logic.V. Michele Abrusci - 1990 - Mathematical Logic Quarterly 36 (1):11-15.
  16.  20
    Function Theory in an Axiom-free Equation Calculus.R. L. Goodstein - 1946 - Journal of Symbolic Logic 11 (1):24-26.
    Direct download  
     
    Export citation  
     
    Bookmark   9 citations  
  17.  57
    An axiomatization of the finite-valued łukasiewicz calculus.Roman Tuziak - 1988 - Studia Logica 47 (1):49 - 55.
    In this paper the completeness theorems for the finite-valued ukasiewicz logics are proved with the use of the Lindenbaum algebra.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  18. A calculus of individuals based on "connection".Bowman L. Clarke - 1981 - Notre Dame Journal of Formal Logic 22 (3):204-218.
    Although Aristotle (Metaphysics, Book IV, Chapter 2) was perhaps the first person to consider the part-whole relationship to be a proper subject matter for philosophic inquiry, the Polish logician Stanislow Lesniewski [15] is generally given credit for the first formal treatment of the subject matter in his Mereology.1 Woodger [30] and Tarski [24] made use of a specific adaptation of Lesniewski's work as a basis for a formal theory of physical things and their parts. The term 'calculus of individuals' (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   69 citations  
  19.  26
    The Calculus of Natural Calculation.René Gazzari - 2021 - Studia Logica 109 (6):1375-1411.
    The calculus of Natural Calculation is introduced as an extension of Natural Deduction by proper term rules. Such term rules provide the capacity of dealing directly with terms in the calculus instead of the usual reasoning based on equations, and therefore the capacity of a natural representation of informal mathematical calculations. Basic proof theoretic results are communicated, in particular completeness and soundness of the calculus; normalisation is briefly investigated. The philosophical impact on a proof theoretic account of (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  20. Differential Calculus Based on the Double Contradiction.Kazuhiko Kotani - 2016 - Open Journal of Philosophy 6 (4):420-427.
    The derivative is a basic concept of differential calculus. However, if we calculate the derivative as change in distance over change in time, the result at any instant is 0/0, which seems meaningless. Hence, Newton and Leibniz used the limit to determine the derivative. Their method is valid in practice, but it is not easy to intuitively accept. Thus, this article describes the novel method of differential calculus based on the double contradiction, which is easier to accept intuitively. (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  21. The Epsilon Calculus.Jeremy Avigad & Richard Zach - 2012 - In Ed Zalta, Stanford Encyclopedia of Philosophy. Stanford, CA: Stanford Encyclopedia of Philosophy.
    The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   22 citations  
  22.  73
    The Calculus of Higher-Level Rules, Propositional Quantification, and the Foundational Approach to Proof-Theoretic Harmony.Peter Schroeder-Heister - 2014 - Studia Logica 102 (6):1185-1216.
    We present our calculus of higher-level rules, extended with propositional quantification within rules. This makes it possible to present general schemas for introduction and elimination rules for arbitrary propositional operators and to define what it means that introductions and eliminations are in harmony with each other. This definition does not presuppose any logical system, but is formulated in terms of rules themselves. We therefore speak of a foundational account of proof-theoretic harmony. With every set of introduction rules a canonical (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  23.  27
    A note to my paper: "On characterizations of the first-order functional calculus".Juliusz Reichbach - 1961 - Notre Dame Journal of Formal Logic 2 (4):251-252.
  24.  16
    Lambda-calculus, combinators, and functional programming.György E. Révész - 1988 - New York: Cambridge University Press.
    Provides computer science students and researchers with a firm background in lambda-calculus and combinators.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  25.  37
    Lambek Calculus with Conjugates.Igor Sedlár & Andrew Tedder - 2020 - Studia Logica 109 (3):447-470.
    We study an expansion of the Distributive Non-associative Lambek Calculus with conjugates of the Lambek product operator and residuals of those conjugates. The resulting logic is well-motivated, under-investigated and difficult to tackle. We prove completeness for some of its fragments and establish that it is decidable. Completeness of the logic is an open problem; some difficulties with applying the usual proof method are discussed.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  26.  18
    (1 other version)The Finite Model Property and Subsystems of Classical Propositional Calculus.Ronald Harrop - 1959 - Mathematical Logic Quarterly 5 (1‐2):29-32.
  27.  39
    An axiomatization of Prior's modal calculus $Q$.R. A. Bull - 1964 - Notre Dame Journal of Formal Logic 5 (3):211-214.
  28. Bernard Nieuwentijt and the Leibnizian calculus.R. H. Vermij - 1989 - Studia Leibnitiana 21 (1):69-86.
    Bernard Nieuwentijt ist in der Mathematikgeschichte bekannt als Kritiker der Leibnizschen Differentialrechnung. Im Gegensatz zu dem, was häufig angenommen wird, war die Kritik an Leibniz' Methode kein Hauptanliegen Nieuwentijts. Das Ziel seines bedeutendsten mathematischen Werks, Analysis infinitorum , war die Systematisierung und logische Deduzierung der ihm bekannten Infinitesimalmethoden, besonders derer von den Engländern wie Barrow, Wallis u. a. Das Werk Leibnizens war ihm anfangs völlig unbekannt. In dem System, das Nieuwentijt selbständig entwarf, rechnete er nicht mit Infinitesimalen höheren Grades: ihre (...)
     
    Export citation  
     
    Bookmark   5 citations  
  29.  42
    Ontology as a natural extension of predicate calculus with identity equipped with description.Toshiharu Waragai - 1990 - Annals of the Japan Association for Philosophy of Science 7 (5):23-40.
  30.  22
    (1 other version)Cut‐Rule Axiomatization of Product‐Free Lambek Calculus With the Empty String.Wojciech Zielonka - 1988 - Mathematical Logic Quarterly 34 (2):135-142.
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  31.  29
    Detleff Clüver: An Early Opponent of the Leibnizian Differential Calculus.Paolo Mancosu & Ezio Vailati - 1990 - Centaurus 33 (3):325-344.
  32.  26
    Belief revision and projection in the epistemic situation calculus.Christoph Schwering, Gerhard Lakemeyer & Maurice Pagnucco - 2017 - Artificial Intelligence 251 (C):62-97.
  33. Sequent calculus in natural deduction style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
    A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  34. Normal Modal Logics In Which The Heyting Propositional Calculus Can Be Embedded.Kosta Dosen - 1988 - Bulletin of the Section of Logic 17 (1):23-30.
     
    Export citation  
     
    Bookmark   4 citations  
  35.  22
    Property persistence in the situation calculus.Ryan F. Kelly & Adrian R. Pearce - 2010 - Artificial Intelligence 174 (12-13):865-888.
  36.  58
    Classical conservative extensions of Lambek calculus.V. Michele Abrusci - 2002 - Studia Logica 71 (3):277 - 314.
  37.  23
    Non-Normal Truth-Tables for the Propositional Calculus.Alonzo Church - 1954 - Journal of Symbolic Logic 19 (3):233-234.
  38. An interpretation of the intuitionistic sentential calculus.K. Gödel - 1969 - In Jaakko Hintikka, The philosophy of mathematics. London,: Oxford University Press.
  39.  66
    Scientific theory as partially interpreted calculus.Brent Mundy - 1987 - Erkenntnis 27 (2):173 - 196.
  40.  14
    (1 other version)Many‐valued modal logics: Uses and predicate calculus.Pascal Ostermann - 1990 - Mathematical Logic Quarterly 36 (4):367-376.
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  41.  45
    Lambda calculus with types.H. P. Barendregt - 2013 - New York: Cambridge University Press. Edited by Wil Dekkers & Richard Statman.
    This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.
    Direct download  
     
    Export citation  
     
    Bookmark   7 citations  
  42.  80
    Normal functors, power series and lambda-calculus.Jean-Yves Girard - 1988 - Annals of Pure and Applied Logic 37 (2):129.
  43.  20
    On characterizations of the first-order functional calculus.Juliusz Reichbach - 1961 - Notre Dame Journal of Formal Logic 2 (1):1-15.
  44.  25
    Structural completeness of the first‐order predicate calculus.W. A. Pogorzelski & T. Prucnal - 1975 - Mathematical Logic Quarterly 21 (1):315-320.
  45. The Quantified Argument Calculus and Natural Logic.Hanoch Ben-Yami - 2020 - Dialectica 74 (2):179-214.
    The formalisation of Natural Language arguments in a formal language close to it in syntax has been a central aim of Moss’s Natural Logic. I examine how the Quantified Argument Calculus (Quarc) can handle the inferences Moss has considered. I show that they can be incorporated in existing versions of Quarc or in straightforward extensions of it, all within sound and complete systems. Moreover, Quarc is closer in some respects to Natural Language than are Moss’s systems – for instance, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  46. A characterization of terms of the λI-calculus having a normal form.Henk Barendregt - 1973 - Journal of Symbolic Logic 38 (3):441-445.
  47.  52
    The Lambek calculus enriched with additional connectives.Makoto Kanazawa - 1992 - Journal of Logic, Language and Information 1 (2):141-171.
    Some formal properties of enriched systems of Lambek calculus with analogues of conjunction and disjunction are investigated. In particular, it is proved that the class of languages recognizable by the Lambek calculus with added intersective conjunction properly includes the class of finite intersections of context-free languages.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  48.  62
    Syntactic calculus with dependent types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
    The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  49.  31
    “Betagraphic”: An Alternative Formulation of Predicate Calculus.Interdisciplinary Seminar on Peirce - 2015 - Transactions of the Charles S. Peirce Society 51 (2):137.
  50.  12
    More about the axiomatics of the Lambek calculus.Wojciech Zielonka - 1997 - Poznan Studies in the Philosophy of the Sciences and the Humanities 57:319-326.
1 — 50 / 941