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
Related categories

29 found
  1. Experimental Mathematics.Alan Baker - 2008 - Erkenntnis 68 (3):331-344.
    The rise of the field of “ experimental 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 experimental mathematics. One suggestion is that experimental mathematics makes essential use of electronic computers. A second suggestion is that experimental 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 third suggestion is (...)
  2. Automated Theorem Proving for Łukasiewicz Logics.Gordon Beavers - 1993 - 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 (...)
  3. Proof-Finding Algorithms for Classical and Subclassical Propositional Logics.M. W. Bunder & R. M. Rizkalla - 2009 - 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. (...)
  4. Computer Proof, Apriori Knowledge, and Other Minds.Tyler Burge - 1998 - Noûs 32 (S12):1-37.
  5. Symbolic Logic and Mechanical Theorem Proving.Chin-Liang Chang - 1973 - 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.
  6. Proof: Its Nature and Significance.Michael Detlefsen - 2008 - In Bonnie Gold & Roger Simons (eds.), Proof and Other Dilemmas: Mathematics and Philosophy. Mathematical Association of America. pp. 1.
    I focus on three preoccupations of recent writings on proof. -/- I. The role and possible effects of empirical reasoning in mathematics. Do recent developments (specifically, the computer-assisted proof of the 4CT) point to something essentially new as regards the need for and/or effects of using broadly empirical and inductive reasoning in mathematics? In particular, should we see such things as the computer-assisted proof of the 4CT as pointing to the existence of mathematical truths of which we cannot have a (...)
  7. The Four-Color Theorem and Mathematical Proof.Michael Detlefsen & Mark Luker - 1980 - Journal of Philosophy 77 (12):803-820.
    I criticize a recent paper by Thomas Tymoczko in which he attributes fundamental philosophical significance and novelty to the lately-published computer-assisted proof of the four color theorem (4CT). Using reasoning precisely analogous to that employed by Tymoczko, I argue that much of traditional mathematical proof must be seen as resting on what Tymoczko must take as being "empirical" evidence. The new proof of the 4CT, with its use of what Tymoczko calls "empirical" evidence is therefore not so novel as he (...)
  8. Reasoning About Partial Functions with the Aid of a Computer.William M. Farmer - 1995 - 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 (...)
  9. A Set Theory with Support for Partial Functions.William M. Farmer & Joshua D. Guttman - 2000 - 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 (...)
  10. Using Mathematica to Understand the Computer Proof of the Robbins Conjecture.Branden Fitelson - manuscript
    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 (...)
  11. Finding Missing Proofs with Automated Reasoning.Branden Fitelson & Larry Wos - 2001 - 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 (...)
  12. An Application of Resolution to Expert Systems: Overcoming Schoenmakers' Paradigm.Joseph S. Fulda - 1994 - 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.
  13. The Logic of Skolem Functions: A Subtle Construction and a Subtle Error.Joseph S. Fulda - 1988 - 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.
  14. The A Priori Meaningfulness Measure and Resolution Theorem Proving.Joseph S. Fulda & Kevin De Fontes - 1989 - 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.
  15. Labelled Resolution for Classical and Non-Classical Logics.D. M. Gabbay & U. Reyle - 1997 - 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 (...)
  16. Connection Tableau Calculi with Disjunctive Constraints.Ortrun Ibens - 2002 - 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 (...)
  17. Reasoning Without Believing: On the Mechanisation of Presuppositions and Partiality.Manfred Kerber & Michael Kohlhase - 2012 - 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.
  18. Mechanical Theorem Proving in a Certain Class of Formulae of the Predicate Calculus.Ewa Orłowska - 1969 - Studia Logica 25 (1):17 - 29.
  19. Identity in Modal Logic Theorem Proving.Francis J. Pelletier - 1993 - 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 (...)
  20. Interest Driven Suppositional Reasoning.John Pollock - manuscript
    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 (...)
  21. Oscar: An Agent Architecture Based on Defeasible Reasoning.John Pollock - manuscript
    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 (...)
  22. Granularity Analysis for Mathematical Proofs.Marvin R. G. Schiller - 2013 - 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 (...)
  23. Metamathematics, Machines, and Gödel's Proof.N. Shankar - 1994 - 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 (...)
  24. Normal Natural Deduction Proofs (in Classical Logic).Wilfried Sieg & John Byrnes - 1998 - 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 (...)
  25. Non-Standard Logics for Automated Reasoning.Philippe Smets (ed.) - 1988 - Academic Press.
  26. Exploratory Experimentation in Experimental Mathematics: A Glimpse at the PSLQ Algorithm.Henrik Kragh Sørensen - 2010 - In Benedikt Löwe & Thomas Müller (eds.), PhiMSAMP. Philosophy of Mathematics: Sociological Aspects and Mathematical Practice. College Publications. pp. 341--360.
    In the present paper, I go beyond these examples by bringing into play an example that I nd more experimental in nature, namely that of the use of the so-called PSLQ algorithm in researching integer relations between numerical constants. It is the purpose of this paper to combine a historical presentation with a preliminary exploration of some philosophical aspects of the notion of experiment in experimental mathematics. This dual goal will be sought by analysing these aspects as they are presented (...)
  27. Computer Proof.Paul Teller - 1980 - Journal of Philosophy 77 (12):797-803.
  28. The Own Character of Mathematics Discussed with Consideration of the Proof of the Four-Color Theorem.W. A. Verloren van Themaat - 1989 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 20 (2):340-350.
    Der Beweis des Vierfarbensatzes mit Hilfe eines Computers, der so viel Zeit erforderte, daß ein Mensch die Berechnungen niemals überprüfen könnte, hat Zweifel erregt an vier philosophischen Annahmen über Mathematik. Die Mathematik ist die Lehre der Klassifikation, insoweit als sie vollständig abstrahiert von der Art der zu klassifizierenden Dinge. Diese Auffassung wird vom Beweis des Vierfarbensatzes nicht erschüttert. Wahrscheinlich kann mathematisches Denken nicht vor sich gehen ohne sinnliche Vorstellungen, aber die Eigenschaften mathematischer Gegenstände sind unabhängig von ihrer Weise sinnlicher Vorstellung.
  29. Proofs Are Programs: 19th Century Logic and 21st Century Computing.Philip Wadler - manuscript
    As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same thing is a story that spans a century, a chase with as (...)