How (and why) to Build an Automated Theorem Prover: De-mystifying Logical Inference

Presentation by Adam Pease at SRI, Menlo Park, CA. I discuss implementation details of writing an automated theorem prover in Java for first order logic. A subsequent video presents questions from the audience and my responses.

[@socialwatcher]

Loved this presentation Adam! We can see the effort and care you put into making JavaRes and also explaining it so clearly to the rest of us. Thank you!

[@blankboy-ww7jt]

Thank you for the video!

[@WarriorStatue]

Thank you for this presentation, it has been very useful while going on my own journey of writing an ATP system based on PyRes

[@adampease]

That's great to hear! Let us know how it goes, and consider entering your prover in CASC

[@WarriorStatue]

@@adampease Thanks, Adam! It's still early stages but I will try my best

[@Treebark1313]

Wonderful presentation, thank you. I'm studying operator theory for an internship, where I'm currently implementing a routine to check the truth value of a particularly involved equivalence relation. This is the first genuinely helpful video resource I've come across.
I can't help but comment at 36:40, as I've never understood partisanship towards certain programming languages. No one is out there claiming Python wins on performance haha, especially against Java. They're different tools for different use cases.

[@adampease]

Many thanks for your kind feedback. I'm so glad this was helpful. I agree completely with your comments about programming languages

[@nathan0temple]

Is it possible to contribute to PyRes?

[@adampease]

yes, you could clone pyres and create your own fork to start with, in order to experiment, then let us know what you'd like to contribute

[@luisramos1977]

I think the term UnitTest is only use in java, not sure about the same name in Python, however we can do test in both.

[@Belissimo-T]

The python standard library unittest module is closely modeled after the respective Java framework.

[@Unique-Concepts]

Hello Prof. I want know is there any limitations of automated theorem prover?

[@adampease]

First order logic with equality is semi-decidable. So in the worst case, it's not guaranteed to terminate, although modern theorem proving systems like E and Vampire usually do terminate if there's a proof for a given query. Of course, the system I've described is the most basic algorithm and not comparable to a modern prover. Every logic has limitations in what it is mathematically capable of representing so any theorem prover working on a particular logic will have the limitations inherent in that logic. For example, Vampire and E, operating on TPTP FOF will be limited to first order - only constant terms and functions denoting terms can be arguments to relations. But both of those systems now support higher order logic in THF as well. Check out my video on Different Logics for more info about this ua-cam.com/video/vre8CrPINrw/v-deo.html

[@Unique-Concepts]

@@adampease Hey thanks prof. For the reply. Could you please suggest any books on Mathematical Logic or may be your favourite books on this subject? Thank you 👏👏👏🙏🙏👌👌

[@adampease]

@@Unique-Concepts - I can suggest my own book Ontology: A Practical Guide, which you can get from ontologyportal.org . To supplement it with more exercises I recommend the Schaums Outlines in Logic workbook - see my course syllabus at ontologyportal.org/course.html and references in the exercizes www.ontologyportal.org/CBS6834.html