About this topic
Summary Computer proofs are those proofs in mathematics that have been at least partially and, sometimes, completely proven by computer. The landmark Appel and Haken proof of the Four Color Theorem in 1976 used a large scale exhaustion-style proof method carried out partially by computer. Shortly before the Appel-Haken proof and up to the present, computer proofs have proven useful both in pure mathematics and areas such as artificial intelligence and machine learning. However, the proof-by-exhaustion methods are contentious in that they represent deductions which are not surveyable by humans in a reasonable amount of time. So, questions for computer proof involve what counts as mathematical proof, are empirical methodologies acceptable in pure mathematics, and do we have certainty that the theorem, etc. proven by computer are indeed proven.
Key works Tymoczko 1979, Burge 1998,  Manders 1989
Introductions Gowers 2008
  Show all references
Related categories
Siblings:
25 found
Search inside:
(import / add options)   Sort by:
  1. Alan Baker (2008). Experimental Mathematics. Erkenntnis 68 (3):331 - 344.
    The rise of the field of “<span class='Hi'>experimental</span> mathematics” poses an apparent challenge to traditional philosophical accounts of mathematics as an a priori, non-empirical endeavor. This paper surveys different attempts to characterize <span class='Hi'>experimental</span> mathematics. One suggestion is that <span class='Hi'>experimental</span> mathematics makes essential use of electronic computers. A second suggestion is that <span class='Hi'>experimental</span> mathematics involves support being gathered for an hypothesis which is inductive rather than deductive. Each of these options turns out to be inadequate, and instead a (...)
    Remove from this list | Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  2. Gordon Beavers (1993). Automated Theorem Proving for Łukasiewicz Logics. Studia Logica 52 (2):183 - 195.
    This paper is concerned with decision proceedures for the 0-valued ukasiewicz logics,. It is shown how linear algebra can be used to construct an automated theorem checker. Two decision proceedures are described which depend on a linear programming package. An algorithm is given for the verification of consequence relations in, and a connection is made between theorem checking in two-valued logic and theorem checking in which implies that determing of a -free formula whether it takes the value one is NP-complete (...)
    Remove from this list | Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  3. M. W. Bunder & R. M. Rizkalla (2009). Proof-Finding Algorithms for Classical and Subclassical Propositional Logics. Notre Dame Journal of Formal Logic 50 (3):261-273.
    The formulas-as-types isomorphism tells us that every proof and theorem, in the intuitionistic implicational logic $H_\rightarrow$, corresponds to a lambda term or combinator and its type. The algorithms of Bunder very efficiently find a lambda term inhabitant, if any, of any given type of $H_\rightarrow$ and of many of its subsystems. In most cases the search procedure has a simple bound based roughly on the length of the formula involved. Computer implementations of some of these procedures were done in Dekker. (...)
    Remove from this list | Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  4. Tyler Burge (1998). Computer Proof, A Priori Knowledge, and Other Minds. Philosophical Perspectives 12 (S12):1-37.
  5. Chin-Liang Chang (1973/1987). Symbolic Logic and Mechanical Theorem Proving. Academic Press.
    This book contains an introduction to symbolic logic and a thorough discussion of mechanical theorem proving and its applications. The book consists of three major parts. Chapters 2 and 3 constitute an introduction to symbolic logic. Chapters 4–9 introduce several techniques in mechanical theorem proving, and Chapters 10 an 11 show how theorem proving can be applied to various areas such as question answering, problem solving, program analysis, and program synthesis.
    Remove from this list |
     
    My bibliography  
     
    Export citation  
  6. William M. Farmer (1995). Reasoning About Partial Functions with the Aid of a Computer. Erkenntnis 43 (3):279 - 294.
    Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper shows how the traditional approach to partial functions (...)
    Remove from this list | Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  7. William M. Farmer & Joshua D. Guttman (2000). A Set Theory with Support for Partial Functions. Studia Logica 66 (1):59-78.
    Partial functions can be easily represented in set theory as certain sets of ordered pairs. However, classical set theory provides no special machinery for reasoning about partial functions. For instance, there is no direct way of handling the application of a function to an argument outside its domain as in partial logic. There is also no utilization of lambda-notation and sorts or types as in type theory. This paper introduces a version of von-Neumann-Bernays-Gödel set theory for reasoning about sets, proper (...)
    Remove from this list | Direct download (9 more)  
     
    My bibliography  
     
    Export citation  
  8. Branden Fitelson, Using Mathematica to Understand the Computer Proof of the Robbins Conjecture.
    mathematicians for over 60 years. Amazingly, the Argonne team's automated theorem-proving program EQP took only 8 days to find a proof of it. Unfortunately, the proof found by EQP is quite complex and difficult to follow. Some of the steps of the EQP proof require highly complex and unintuitive substitution strategies. As a result, it is nearly impossible to reconstruct or verify the computer proof of the Robbins conjecture entirely by hand. This is where the unique symbolic capabilities of Mathematica (...)
    Remove from this list | Direct download  
     
    My bibliography  
     
    Export citation  
  9. Branden Fitelson & Larry Wos (2001). Finding Missing Proofs with Automated Reasoning. Studia Logica 68 (3):329-356.
    This article features long-sought proofs with intriguing properties (such as the absence of double negation and the avoidance of lemmas that appeared to be indispensable), and it features the automated methods for finding them. The theorems of concern are taken from various areas of logic that include two-valued sentential (or propositional) calculus and infinite-valued sentential calculus. Many of the proofs (in effect) answer questions that had remained open for decades, questions focusing on axiomatic proofs. The approaches we take are of (...)
    Remove from this list | Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  10. Joseph S. Fulda (1994). An Application of Resolution to Expert Systems: Overcoming Schoenmakers' Paradigm. Association for Automated Reasoning Newsletter 25:10-12.
    The full-text of the entire issue is available on the Web; readers seeing this should ensure that there is permission to download. It would be quite difficult to separate just my piece from the others.
    Remove from this list |
     
    My bibliography  
     
    Export citation  
  11. Joseph S. Fulda (1988). The Logic of Skolem Functions: A Subtle Construction and a Subtle Error. Association for Automated Reasoning Newsletter 10:5-6.
    The full-text of the entire issue is available on the Web; readers seeing this should ensure that there is permission to download. It would be quite difficult to separate just my piece from the others.
    Remove from this list |
     
    My bibliography  
     
    Export citation  
  12. Joseph S. Fulda & Kevin De Fontes (1989). The A Priori Meaningfulness Measure and Resolution Theorem Proving. Journal of Experimental and Theoretical Artificial Intelligence 1 (3):227-230.
    Demonstrates the validity of the measure presented in "Estimating Semantic Content" on textbook examples using (binary) resolution [a generalization of disjunctive syllogism] theorem proving; the measure is based on logical probability and is the mirror image of logical form; it dates to Popper.
    Remove from this list | Direct download  
     
    My bibliography  
     
    Export citation  
  13. D. M. Gabbay & U. Reyle (1997). Labelled Resolution for Classical and Non-Classical Logics. Studia Logica 59 (2):179-216.
    Resolution is an effective deduction procedure for classical logic. There is no similar "resolution" system for non-classical logics (though there are various automated deduction systems). The paper presents resolution systems for intuistionistic predicate logic as well as for modal and temporal logics within the framework of labelled deductive systems. Whereas in classical predicate logic resolution is applied to literals, in our system resolution is applied to L(abelled) R(epresentation) S(tructures). Proofs are discovered by a refutation procedure defined on LRSs, that imposes (...)
    Remove from this list | Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  14. Ortrun Ibens (2002). Connection Tableau Calculi with Disjunctive Constraints. Studia Logica 70 (2):241 - 270.
    Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling of constraints during (...)
    Remove from this list | Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  15. Manfred Kerber & Michael Kohlhase (2012). Reasoning Without Believing: On the Mechanisation of Presuppositions and Partiality. Journal of Applied Non-Classical Logics 22 (4):295 - 317.
    (2012). Reasoning without believing: on the mechanisation of presuppositions and partiality. Journal of Applied Non-Classical Logics: Vol. 22, No. 4, pp. 295-317. doi: 10.1080/11663081.2012.705962.
    Remove from this list | Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  16. Ewa Orłowska (1969). Mechanical Theorem Proving in a Certain Class of Formulae of the Predicate Calculus. Studia Logica 25 (1):17 - 29.
  17. Francis J. Pelletier (1993). Identity in Modal Logic Theorem Proving. Studia Logica 52 (2):291 - 308.
    THINKER is an automated natural deduction first-order theorem proving program. This paper reports on how it was adapted so as to prove theorems in modal logic. The method employed is an indirect semantic method, obtained by considering the semantic conditions involved in being a valid argument in these modal logics. The method is extended from propositional modal logic to predicate modal logic, and issues concerning the domain of quantification and existence in a world's domain are discussed. Finally, we look at (...)
    Remove from this list | Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  18. John Pollock, Interest Driven Suppositional Reasoning.
    The aim of this paper is to investigate two related aspects of human reasoning, and use the results to construct an automated theorem prover for the predicate calculus that at least approximately models human reasoning. The result is a non-resolution theorem prover that does not use Skolemization. It involves two central ideas. One is the interest constraints that are of central importance in guiding human reasoning. The other is the notion of suppositional reasoning, wherein one makes a supposition, draws inferences (...)
    Remove from this list | Direct download  
     
    My bibliography  
     
    Export citation  
  19. John Pollock, Oscar: An Agent Architecture Based on Defeasible Reasoning.
    Proceedings of the 2008 AAAI Spring Symposium on Architectures for Intelligent Theory-Based Agents. “OSCAR is a fully implemented architecture for a cognitive agent, based largely on the author’s work in philosophy concerning epistemology and practical cognition. The seminal idea is that a generally intelligent agent must be able to function in an environment in which it is ignorant of most matters of fact. The architecture incorporates a general-purpose defeasible reasoner, built on top of an efficient natural deduction reasoner for first-order (...)
    Remove from this list | Direct download  
     
    My bibliography  
     
    Export citation  
  20. Marvin R. G. Schiller (2013). Granularity Analysis for Mathematical Proofs. Topics in Cognitive Science 5 (2):251-269.
    Mathematical proofs generally allow for various levels of detail and conciseness, such that they can be adapted for a particular audience or purpose. Using automated reasoning approaches for teaching proof construction in mathematics presupposes that the step size of proofs in such a system is appropriate within the teaching context. This work proposes a framework that supports the granularity analysis of mathematical proofs, to be used in the automated assessment of students' proof attempts and for the presentation of hints and (...)
    Remove from this list | Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  21. N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
    The automatic verification of large parts of mathematics has been an aim of many mathematicians from Leibniz to Hilbert. While Gödel's first incompleteness theorem showed that no computer program could automatically prove certain true theorems in mathematics, the advent of electronic computers and sophisticated software means in practice there are many quite effective systems for automated reasoning that can be used for checking mathematical proofs. This book describes the use of a computer program to check the proofs of several celebrated (...)
    Remove from this list |
     
    My bibliography  
     
    Export citation  
  22. Wilfried Sieg & John Byrnes (1998). Normal Natural Deduction Proofs (in Classical Logic). Studia Logica 60 (1):67-106.
    Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically motivated ways? This informal (...)
    Remove from this list | Direct download (12 more)  
     
    My bibliography  
     
    Export citation  
  23. Philippe Smets (ed.) (1988). Non-Standard Logics for Automated Reasoning. Academic Press.
    Remove from this list |
     
    My bibliography  
     
    Export citation  
  24. Paul Teller (1980). Computer Proof. Journal of Philosophy 77 (12):797-803.
    Remove from this list | Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  25. W. A. Verloren van Themaat (1989). The Own Character of Mathematics Discussed with Consideration of the Proof of the Four-Color Theorem. Journal for General Philosophy of Science 20 (2):340-350.
    Remove from this list | Direct download (4 more)  
     
    My bibliography  
     
    Export citation