This category needs an editor. We encourage you to help if you are qualified.
Volunteer, or read more about what this involves.
Related categories

41 found
Order:
  1. First Order Logic with Empty Structures.Mohamed A. Amer - 1989 - Studia Logica 48 (2):169 - 177.
    For first order languages with no individual constants, empty structures and truth values (for sentences) in them are defined. The first order theories of the empty structures and of all structures (the empty ones included) are axiomatized with modus ponens as the only rule of inference. Compactness is proved and decidability is discussed. Furthermore, some well known theorems of model theory are reconsidered under this new situation. Finally, a word is said on other approaches to the whole problem.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  2. Computational Logic. Vol. 1: Classical Deductive Computing with Classical Logic.Luis M. Augusto - 2018 - London: College Publications.
    This is the first of a two-volume work combining two fundamental components of contemporary computing into classical deductive computing, a powerful form of computation, highly adequate for programming and automated theorem proving, which, in turn, have fundamental applications in areas of high complexity and/or high security such as mathematical proof, software specification and verification, and expert systems. Deductive computation is concerned with truth-preservation: This is the essence of the satisfiability problem, or SAT, the central computational problem in computability and complexity (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  3. Lógicas multivalentes. Uma introdução matemática e computacional.Luis M. Augusto - 2016 - Dissertation, Universidade Aberta
    This is a mathematical and computational intro to many-valued logics. The approach is mostly mathematical, namely algebraic (via the notion of logical matrix) and computational (via the satisfiability problem). An automated calculus -- the signed resolution calculus for many-valued logics -- is elaborated on.
    Remove from this list  
    Translate
     
     
    Export citation  
     
    Bookmark  
  4. Some Jump-Like Operations in $\Mathbf \Beta $-Recursion Theory.Colin G. Bailey - 2013 - Journal of Symbolic Logic 78 (1):57-71.
    In this paper we show that there are various pseudo-jump operators definable over inadmissible $J_{\beta}$ that relate to the failure of admissiblity and to non-regularity. We will use these ideas to construct some intermediate degrees.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  5. Effective Coloration.Dwight R. Bean - 1976 - Journal of Symbolic Logic 41 (2):469-480.
    We are concerned here with recursive function theory analogs of certain problems in chromatic graph theory. The motivating question for our work is: Does there exist a recursive (countably infinite) planar graph with no recursive 4-coloring? We obtain the following results: There is a 3-colorable, recursive planar graph which, for all k, has no recursive k-coloring; every decidable graph of genus p ≥ 0 has a recursive 2(χ(p) - 1)-coloring, where χ(p) is the least number of colors which will suffice (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  6. Proving Consistency of Equational Theories in Bounded Arithmetic.Arnold Beckmann - 2002 - Journal of Symbolic Logic 67 (1):279-296.
    We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S 1 2 . In particular this solves an open problem formulated by TAKEUTI (c.f. [5, p.5 problem 9.]).
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7. The Unprovability in Intuitionistic Formal Systems of the Continuity of Effective Operations on the Reals.Michael Beeson - 1976 - Journal of Symbolic Logic 41 (1):18-24.
  8. On the Induction Schema for Decidable Predicates.Lev D. Beklemishev - 2003 - Journal of Symbolic Logic 68 (1):17-34.
    We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, $I\Delta_1$ . We show that $I\Delta_1$ is independent from the set of all true arithmetical $\Pi_2-sentences$ . Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also obtain some conservation and independence results for parameter free and inference rule forms of $\Delta_1-induction$ . An open problem formulated by J. (...)
    Remove from this list   Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  9. Modal Logic.Patrick Blackburn, Maarten de Rijke & Yde Venema - 2002 - Cambridge University Press.
    This modern, advanced textbook reviews modal logic, a field which caught the attention of computer scientists in the late 1970's.
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   191 citations  
  10. On the Recursive Unsolvability of the Provability of the Deduction Theorem in Partial Propositional Calculi.D. Bollman & M. Tapia - 1972 - Notre Dame Journal of Formal Logic 13 (1):124-128.
  11. From the Closed Classical Algorithmic Universe to an Open World of Algorithmic Constellations.Mark Burgin & Gordana Dodig-Crnkovic - 2013 - In Gordana Dodig-Crnkovic Raffaela Giovagnoli (ed.), Computing Nature. pp. 241--253.
    In this paper we analyze methodological and philosophical implications of algorithmic aspects of unconventional computation. At first, we describe how the classical algorithmic universe developed and analyze why it became closed in the conventional approach to computation. Then we explain how new models of algorithms turned the classical closed algorithmic universe into the open world of algorithmic constellations, allowing higher flexibility and expressive power, supporting constructivism and creativity in mathematical modeling. As Goedels undecidability theorems demonstrate, the closed algorithmic universe restricts (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  12. On the Mosaic Method for Many-Dimensional Modal Logics: A Case Study Combining Tense and Modal Operators. [REVIEW]Carlos Caleiro, Luca Viganò & Marco Volpe - 2013 - Logica Universalis 7 (1):33-69.
    We present an extension of the mosaic method aimed at capturing many-dimensional modal logics. As a proof-of-concept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5-like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof of completeness (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  13. Discontinuities of Provably Correct Operators on the Provably Recursive Real Numbers.William J. Collins & Paul Young - 1983 - Journal of Symbolic Logic 48 (4):913-920.
    In this paper we continue, from [2], the development of provably recursive analysis, that is, the study of real numbers defined by programs which can be proven to be correct in some fixed axiom system S. In particular we develop the provable analogue of an effective operator on the set C of recursive real numbers, namely, a provably correct operator on the set P of provably recursive real numbers. In Theorems 1 and 2 we exhibit a provably correct operator on (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  14. Storage Operators and Directed Lambda-Calculus.René David & Karim Nour - 1995 - Journal of Symbolic Logic 60 (4):1054-1086.
    Storage operators have been introduced by J. L. Krivine in [5] they are closed λ-terms which, for a data type, allow one to simulate a "call by value" while using the "call by name" strategy. In this paper, we introduce the directed λ-calculus and show that it has the usual properties of the ordinary λ-calculus. With this calculus we get an equivalent--and simple--definition of the storage operators that allows to show some of their properties: $\bullet$ the stability of the set (...)
    Remove from this list   Direct download (9 more)  
     
    Export citation  
     
    Bookmark  
  15. A Contradiction and P=NP Problem.Farzad Didehvar - manuscript
    Here, by introducing a version of “Unexpected hanging paradox” first we try to open a new way and a new explanation for paradoxes, similar to liar paradox. Also, we will show that we have a semantic situation which no syntactical logical system could support it. Finally, we propose a claim in Theory of Computation about the consistency of this Theory. One of the major claim is:Theory of Computation and Classical Logic leads us to a contradiction.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  16. Explaining Experience In Nature: The Foundations Of Logic And Apprehension.Steven Ericsson-Zenith - forthcoming - Institute for Advanced Science & Engineering.
    At its core this book is concerned with logic and computation with respect to the mathematical characterization of sentient biophysical structure and its behavior. -/- Three related theories are presented: The first of these provides an explanation of how sentient individuals come to be in the world. The second describes how these individuals operate. And the third proposes a method for reasoning about the behavior of individuals in groups. -/- These theories are based upon a new explanation of experience in (...)
    Remove from this list  
    Translate
     
     
    Export citation  
     
    Bookmark  
  17. What is an Algorithm.Yuri Gurevich - 2012 - Lecture Notes in Computer Science.
  18. Simple or Complex Bodies? Trade-Offs in Exploiting Body Morphology for Control.Matej Hoffmann & Vincent C. Müller - 2017 - In Gordana Dodig-Crnkovic & Raffaela Giovagnoli (eds.), Representation of Reality: Humans, Other Living Organisms and Intelligent Machines. Berlin: Springer. pp. 335-345.
    Engineers fine-tune the design of robot bodies for control purposes, however, a methodology or set of tools is largely absent, and optimization of morphology (shape, material properties of robot bodies, etc.) is lagging behind the development of controllers. This has become even more prominent with the advent of compliant, deformable or ”soft” bodies. These carry substantial potential regarding their exploitation for control—sometimes referred to as ”morphological computation”. In this article, we briefly review different notions of computation by physical systems and (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  19. Recursion in Kolmogorov's R-Operator and the Ordinal Σ.Thomas John - 1986 - Journal of Symbolic Logic 51 (1):1 - 11.
  20. Computability and Complexity: From a Programming Perspective Vol. 21.N. D. Jones - 1997 - MIT Press.
    This makes his book especially valuable." -- Yuri Gurevich, Professor of Computer Science, University of Michigan Computability and complexity theory should be of central concern to practitioners as well as theorists.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  21. The Church-Turing ‘Thesis’ as a Special Corollary of Gödel’s Completeness Theorem.Saul A. Kripke - 2013 - In B. J. Copeland, C. Posy & O. Shagrir (eds.), Computability: Turing, Gödel, Church, and Beyond. MIT Press.
    Traditionally, many writers, following Kleene (1952), thought of the Church-Turing thesis as unprovable by its nature but having various strong arguments in its favor, including Turing’s analysis of human computation. More recently, the beauty, power, and obvious fundamental importance of this analysis, what Turing (1936) calls “argument I,” has led some writers to give an almost exclusive emphasis on this argument as the unique justification for the Church-Turing thesis. In this chapter I advocate an alternative justification, essentially presupposed by Turing (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  22. A Theory Explains Deep Learning.Kenneth Kijun Lee & Chase Kihwan Lee - manuscript
    This is our journal for developing Deduction Theory and studying Deep Learning and Artificial intelligence. Deduction Theory is a Theory of Deducing World’s Relativity by Information Coupling and Asymmetry. We focus on information processing, see intelligence as an information structure that relatively close object-oriented, probability-oriented, unsupervised learning, relativity information processing and massive automated information processing. We see deep learning and machine learning as an attempt to make all types of information processing relatively close to probability information processing. We will discuss (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  23. A Turing Machine for Exponential Function.P. M. F. Lemos - manuscript
    This is a Turing Machine which computes the exponential function f(x,y) = xˆy. Instructions format and operation of this machine are intended to best reflect the basic conditions outlined by Alan Turing in his On Computable Numbers, with an Application to the Entscheidungsproblem (1936), using the simplest single-tape and single-symbol version, in essence due to Kleene (1952) and Carnielli & Epstein (2008). This machine is composed by four basic task machines: one which checks if exponent y is zero, a second (...)
    Remove from this list   Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark  
  24. The Social in the Platform Trap: Why a Microscopic System Focus Limits the Prospect of Social Machines.Markus Luczak-Roesch & Ramine Tinati - 2017 - Discover Society 40.
    “Filter bubble”, “echo chambers”, “information diet” – the metaphors to describe today’s information dynamics on social media platforms are fairly diverse. People use them to describe the impact of the viral spread of fake, biased or purposeless content online, as witnessed during the recent race for the US presidency or the latest outbreak of the Ebola virus (in the latter case a tasteless racist meme was drowning out any meaningful content). This unravels the potential envisioned to arise from emergent activities (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  25. A Universal Socio-Technical Computing Machine.Markus Luczak-Roesch, Ramine Tinati, Saud Aljaloud, Wendy Hall & Nigel Shadbolt - 2016 - In International Conference on Web Engineering.
    This is an attempt to develop a universal socio-technical computing machine that captures and coordinates human input to let collective problem solving activities emerge on the Web without the need for an a priori composition of a dedicated task or human collective.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  26. Socio-Technical Computation.Markus Luczak-Roesch, Ramine Tinati, Kieron O'Hara & Nigel Shadbolt - 2015 - In Proceedings of the 18th ACM Conference Companion on Computer Supported Cooperative Work & Social Computing.
    Motivated by the significant amount of successful collaborative problem solving activity on the Web, we ask: Can the accumulated information propagation behavior on the Web be conceived as a giant machine, and reasoned about accordingly? In this paper we elaborate a thesis about the computational capability embodied in information sharing activities that happen on the Web, which we term socio-technical computation, reflecting not only explicitly conditional activities but also the organic potential residing in information on the Web.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  27. The Metatheory of the Classical Propositional Calculus is Not Axiomatizable.Ian Mason - 1985 - Journal of Symbolic Logic 50 (2):451-457.
  28. Computational Speed-Up by Effective Operators.Albert R. Meyer & Patrick C. Fischer - 1972 - Journal of Symbolic Logic 37 (1):55-68.
  29. What a Course on Philosophy of Computing is Not.Vincent C. Müller - 2008 - APA Newsletter on Philosophy and Computers 8 (1):36-38.
    Immanuel Kant famously defined philosophy to be about three questions: “What can I know? What should I do? What can I hope for?” (KrV, B833). I want to suggest that the three questions of our course on the philosophy of computing are: What is computing? What should we do with computing? What could computing do?
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  30. A Guarded Fragment for Abstract State Machines.Antje Nowack - 2005 - Journal of Logic, Language and Information 14 (3):345-368.
    Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods. Applications of this method motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to (...)
    Remove from this list   Direct download (10 more)  
     
    Export citation  
     
    Bookmark  
  31. Defining a Decidability Decider for the Halting Problem.Pete Olcott - manuscript
    When we understand that every potential halt decider must derive a formal mathematical proof from its inputs to its final states previously undiscovered semantic details emerge. -/- When-so-ever the potential halt decider cannot derive a formal proof from its input strings to its final states of Halts or Loops, undecidability has been decided. -/- The formal proof involves tracing the sequence of state transitions of the input TMD as syntactic logical consequence inference steps in the formal language of Turing Machine (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  32. Intractability and the Use of Heuristics in Psychological Explanations.Iris Rooij, Cory Wright & Todd Wareham - 2012 - Synthese 187 (2):471-487.
  33. Aspectos psico-bio-socio-culturales del lenguaje natural humano.Dante Roberto Salatino (ed.) - 2012 - Desktop Publishing Amazon.
    Este estudio del lenguaje natural, realizado desde la observación, permite analizar los aspectos subjetivos que le dan origen al lenguaje, y que posibilitan su adquisición y comprensión. Como tal constituye la primera teoría realmente original aparecida en los últimos 55 años, luego que Chomsky nos hiciera conocer su gramática generativa (1957), con la diferencia que, en este caso, tiene el soporte de una lógica también original, la Lógica Transcursiva. Esta lógica se basa en una modificación de la lógica policontextural de (...)
    Remove from this list   Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark  
  34. Higher Order Numerical Differentiation on the Infinity Computer.Yaroslav Sergeyev - 2011 - Optimization Letters 5 (4):575-585.
    There exist many applications where it is necessary to approximate numerically derivatives of a function which is given by a computer procedure. In particular, all the fields of optimization have a special interest in such a kind of information. In this paper, a new way to do this is presented for a new kind of a computer - the Infinity Computer - able to work numerically with finite, infinite, and infinitesimal number. It is proved that the Infinity Computer is able (...)
    Remove from this list   Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  35. Numerical Computations and Mathematical Modelling with Infinite and Infinitesimal Numbers.Yaroslav Sergeyev - 2009 - Journal of Applied Mathematics and Computing 29:177-195.
    Traditional computers work with finite numbers. Situations where the usage of infinite or infinitesimal quantities is required are studied mainly theoretically. In this paper, a recently introduced computational methodology (that is not related to the non-standard analysis) is used to work with finite, infinite, and infinitesimal numbers numerically. This can be done on a new kind of a computer – the Infinity Computer – able to work with all these types of numbers. The new computational tools both give possibilities to (...)
    Remove from this list   Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark  
  36. Single-Tape and Multi-Tape Turing Machines Through the Lens of the Grossone Methodology.Yaroslav Sergeyev & Alfredo Garro - 2013 - Journal of Supercomputing 65 (2):645-663.
    The paper investigates how the mathematical languages used to describe and to observe automatic computations influence the accuracy of the obtained results. In particular, we focus our attention on Single and Multi-tape Turing machines which are described and observed through the lens of a new mathematical language which is strongly based on three methodological ideas borrowed from Physics and applied to Mathematics, namely: the distinction between the object (we speak here about a mathematical object) of an observation and the instrument (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  37. Reasoning About Truth in First-Order Logic.Claes Strannegård, Fredrik Engström, Abdul Rahim Nizamani & Lance Rips - 2013 - Journal of Logic, Language and Information 22 (1):115-137.
    First, we describe a psychological experiment in which the participants were asked to determine whether sentences of first-order logic were true or false in finite graphs. Second, we define two proof systems for reasoning about truth and falsity in first-order logic. These proof systems feature explicit models of cognitive resources such as declarative memory, procedural memory, working memory, and sensory memory. Third, we describe a computer program that is used to find the smallest proofs in the aforementioned proof systems when (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  38. Introduction to Mathematical Logic.Michał Walicki - 2012 - World Scientific.
    A history of logic -- Patterns of reasoning -- A language and its meaning -- A symbolic language -- 1850-1950 mathematical logic -- Modern symbolic logic -- Elements of set theory -- Sets, functions, relations -- Induction -- Turning machines -- Computability and decidability -- Propositional logic -- Syntax and proof systems -- Semantics of PL -- Soundness and completeness -- First order logic -- Syntax and proof systems of FOL -- Semantics of FOL -- More semantics -- Soundness and (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  39. A Virtual Solution to the Frame Problem.Jonathan A. Waskan - forthcoming - Proceedings of the First IEEE-RAS International Conference on Humanoid Robots.
    We humans often respond effectively when faced with novel circumstances. This is because we are able to predict how particular alterations to the world will play out. Philosophers, psychologists, and computational modelers have long favored an account of this process that takes its inspiration from the truth-preserving powers of formal deduction techniques. There is, however, an alternative hypothesis that is better able to account for the human capacity to predict the consequences worldly alterations. This alternative takes its inspiration from the (...)
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  40. Jump Operator and Yates Degrees.Guohua Wu - 2006 - Journal of Symbolic Logic 71 (1):252 - 264.
    In [9]. Yates proved the existence of a Turing degree a such that 0. 0′ are the only c.e. degrees comparable with it. By Slaman and Steel [7], every degree below 0′ has a 1-generic complement, and as a consequence. Yates degrees can be 1-generic, and hence can be low. In this paper, we prove that Yates degrees occur in every jump class.
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  41. Strong Normalization of a Symmetric Lambda Calculus for Second-Order Classical Logic.Yoriyuki Yamagata - 2002 - Archive for Mathematical Logic 41 (1):91-99.
    We extend Barbanera and Berardi’s symmetric lambda calculus to second order classical propositional logic and prove its strong normalization.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark