Switch to: References

Citations of:

An improved proof procedure

Theoria 26 (2):102-139 (1960)

Add citations

You must login to add citations.
  1. A tableau calculus for partial functions.Manfred Kerber Michael Kohlhase - unknown
    Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Condensed detachment as a rule of inference.J. A. Kalman - 1983 - Studia Logica 42 (4):443 - 451.
    Condensed detachment is usually regarded as a notation, and defined by example. In this paper it is regarded as a rule of inference, and rigorously defined with the help of the Unification Theorem of J. A. Robinson. Historically, however, the invention of condensed detachment by C. A. Meredith preceded Robinson's studies of unification. It is argued that Meredith's ideas deserve recognition in the history of unification, and the possibility that Meredith was influenced, through ukasiewicz, by ideas of Tarski going back (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Logic in mathematics and computer science.Richard Zach - forthcoming - In Filippo Ferrari, Elke Brendel, Massimiliano Carrara, Ole Hjortland, Gil Sagi, Gila Sher & Florian Steinberger (eds.), Oxford Handbook of Philosophy of Logic. Oxford, UK: Oxford University Press.
    Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but have been (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Computer proofs of limit theorems.W. W. Bledsoe, R. S. Boyer & W. H. Henneman - 1972 - Artificial Intelligence 3 (C):27-60.
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Necessity of Thought.Cesare Cozzo - 2014 - In Heinrich Wansing (ed.), Dag Prawitz on Proofs and Meaning. Cham, Switzerland: Springer. pp. 101-20.
    The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Non-resolution theorem proving.W. W. Bledsoe - 1977 - Artificial Intelligence 9 (1):1-35.
    Download  
     
    Export citation  
     
    Bookmark   41 citations  
  • Doing arithmetic without diagrams.F. Malloy Brown - 1977 - Artificial Intelligence 8 (2):175-200.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • An experimental logic based on the fundamental deduction principle.Frank M. Brown - 1986 - Artificial Intelligence 30 (2):117-263.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • A history of theoria.Sven Ove Hansson - 2009 - Theoria 75 (1):2-27.
    Theoria , the international Swedish philosophy journal, was founded in 1935. Its contributors in the first 75 years include the major Swedish philosophers from this period and in addition a long list of international philosophers, including A. J. Ayer, C. D. Broad, Ernst Cassirer, Hector Neri Castañeda, Arthur C. Danto, Donald Davidson, Nelson Goodman, R. M. Hare, Carl G. Hempel, Jaakko Hintikka, Saul Kripke, Henry E. Kyburg, Keith Lehrer, Isaac Levi, David Lewis, Gerald MacCallum, Richard Montague, Otto Neurath, Arthur N. (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Group Cancellation and Resolution.Alessandra Carbone - 2006 - Studia Logica 82 (1):73-93.
    We establish a connection between the geometric methods developed in the combinatorial theory of small cancellation and the propositional resolution calculus. We define a precise correspondence between resolution proofs in logic and diagrams in small cancellation theory, and as a consequence, we derive that a resolution proof is a 2-dimensional process. The isoperimetric function defined on diagrams corresponds to the length of resolution proofs.
    Download  
     
    Export citation  
     
    Bookmark  
  • Some Recent Developments in Complete Strategies for Theorem‐Proving by Computer.Bernard Meltzer - 1968 - Mathematical Logic Quarterly 14 (25-29):377-382.
    Download  
     
    Export citation  
     
    Bookmark  
  • First-Order Tableaux with Sorts.Christoph Weidenbach - 1995 - Logic Journal of the IGPL 3 (6):887-906.
    In this article first-order semantic tableaux and free variable tableaux are extended with sorts. Sorts are sets of unary predicates. They can be attached to variables. Semantically, the domain of a variable is restricted to the intersection of the denotations of the attached predicates. Syntactically, the sort information is exploited by modified γ and δ tableaux rules. The standard unification algorithm of free variable tableaux is replaced by a sorted unification algorithm. The resulting calculi, tableaux with sorts and free variable (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Hilbert's epsilon as an operator of indefinite committed choice.Claus-Peter Wirth - 2008 - Journal of Applied Logic 6 (3):287-317.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Towards the automation of set theory and its logic.Frank Malloy Brown - 1978 - Artificial Intelligence 10 (3):281-316.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Editor’s Introduction to Jean van Heijenoort, Historical Development of Modern Logic.Irving H. Anellis - 2012 - Logica Universalis 6 (3-4):301-326.
    Van Heijenoort’s account of the historical development of modern logic was composed in 1974 and first published in 1992 with an introduction by his former student. What follows is a new edition with a revised and expanded introduction and additional notes.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Using rewriting rules for connection graphs to prove theorems.C. L. Chang & J. R. Slagle - 1979 - Artificial Intelligence 12 (2):159-178.
    Download  
     
    Export citation  
     
    Bookmark   1 citation