Topics Logic

Question Do philosophers use computers to find logical proofs? Or are there good reasons the task of programming a computer to do so is difficult (perhaps because of the complexity of proof required, or perhaps because you need a human for some sort of creative step)? Just from my experience of undergrad logic, it seemed to me there was a lot of repetition in what I was doing, and that it was a task I could learn and get better in -- ie, it wasn't down to pure creativity, but there were learnable, repeatable methods of searching that perhaps could be codified, made systematic.

Accepted:
September 30, 2016

Comments

The short answer to your

The short answer to your first question is "not usually". The short answer to your second question is: It is difficult because of the complexity of the proof. Verifying a proof is, indeed, "codifiable" ("computable" is the technical term) and relatively easy to program (with an emphasis on "relatively"!). Creating proofs is rather more difficult but can also be done, especially if the formula to be proved is already known to be provable. Finding new proofs of unproved propositions has also been done, but is considerably more difficult and is the focus much research in what is called "automated theorem proving".

One of, if not the, first AI programs was the Logic Theorist, developed by Nobel-prize winner Herbert Simon, Allen Newell, and Cliff Shaw, in 1955. So this is an area that has indeed been looked at. A rule of inference known as "resolution" is used in automated theorem proving and lies at the foundation of the Prolog programming language ("Prolog" = "PROgramming in LOGic").

When computers for the general public were first being made available in the 1980s, my colleagues and I wrote a logic textbook called "Logic: A Computer Approach" which showed students how to write programs that would verify and generate (simple) proofs.
It's out of print but used copies can be found online: https://www.amazon.com/Logic-Computer-Approach-Morton-Schagrin/dp/007055...

You can find more information on computational logic by doing a Google search or a Wikipedia search for some of the terms I used above. A classic textbook on automated theorem proving is Chang & Lee's "Symbolic Logic and Mechanical Theorem Proving" (amazon.com/Symbolic-Mechanical-Theorem-Computer-Mathematics/dp/0121703509/). For recent AI research on the topic, go to AI Topics at http://aitopics.org/search/site/automated%20theorem%20proving