6
$\begingroup$

I'm interested in writing my undergraduate thesis on automated theorem proving, and I've been looking for some material to document myself on the topic.

I was introduced to automated and assisted theorem proving by reading a few books that describe the idea to non-necessarily-technical readers, but they were written between the 1970s and the 80s, and most technical books I am finding on the topic are from that same period. That's not to say that old books are not good, most math books I own are reprints of books from that very period, I'm just wondering whether or not the topic has been of any interest to researchers in the last few years.

If it hasn't, why do you think this is the case? And if it has, what do you think would be a good starting point for me to dive into it?

Improve this question
$\endgroup$
5
  • $\begingroup$ I think the issue is much more of a "too much going on to summarize" than the opposite. I'm a bit concerned about references to the 70s and 80s, since almost all of the wikipedia references are more recent. en.wikipedia.org/wiki/Automated_theorem_proving How exactly did you search for this? $\endgroup$
    – cody
    Jun 24, 2022 at 17:40
  • $\begingroup$ @cody I have been looking for books specifically, I admit I have not looked at the wikipedia references... I'll have a look. As for the "too much going on", do you have any particular suggestion as for what could be a starting point to get to know the subject? $\endgroup$
    – mell_o_tron
    Jun 24, 2022 at 17:50
  • $\begingroup$ The Handbook of Automated Reasoning provides a pretty good intro to the research-level issues, but may be too introductory or too advanced depending on your background: sciencedirect.com/book/9780444508133/… $\endgroup$
    – cody
    Jun 24, 2022 at 19:06
  • 1
    $\begingroup$ It's a mere 2000 pages, and a bit outdated since it's over 20 years old, but a lot of this still holds up. $\endgroup$
    – cody
    Jun 24, 2022 at 19:09
  • $\begingroup$ And it doesn't even touch SMT, which is a huge field as well... en.wikipedia.org/wiki/Satisfiability_modulo_theories $\endgroup$
    – cody
    Jun 24, 2022 at 19:17

1 Answer 1

Reset to default
1
$\begingroup$

I would suggest you to have a look at modern implementations of open source theorem provers frameworks, such as Lean and Coq. From there you can have a look into their bibliography to find relevant manuscripts.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I recently discovered both lean and coq, and they seem to be what I've been looking for. Thanks :) $\endgroup$
    – mell_o_tron
    Jul 1, 2022 at 18:20
  • 6
    $\begingroup$ Neither Lean nor Coq are automated theorem provers though, they are interactive proof checkers. The Handbook of Satisfiability by Heule, Kullmann, Wieringa, Biere, is a relatively recent look at modern SAT solvers, the workhorse of all automated theorem provers, including proof automation in interactive systems like Lean. $\endgroup$
    – Martin Berger
    Jul 1, 2022 at 21:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.