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!
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.
In your first example with an attractive blue car. I still dont get why not just direct proof? The contradiction is just a layer around. You ended up concluding attractive(by modus ponens), only discharging your hypothetical at the very end
By a "direct proof" I'm guessing you mean some sort of Natural Deduction method? That's certainly possible, at least in this case, but that a different proof method than proof by contradiction, which is the method that all high-performance ATP systems use these days. Other styles of proof are easier to read but method of proof by contradiction are the fastest. If I'm misunderstanding your question though, I'd be eager for clarification.
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 ruclips.net/video/vre8CrPINrw/видео.html
@@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 👏👏👏🙏🙏👌👌
@@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
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!
Thank you for this presentation, it has been very useful while going on my own journey of writing an ATP system based on PyRes
That's great to hear! Let us know how it goes, and consider entering your prover in CASC
@@adampease Thanks, Adam! It's still early stages but I will try my best
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.
Many thanks for your kind feedback. I'm so glad this was helpful. I agree completely with your comments about programming languages
Thank you for the video!
Is it possible to contribute to PyRes?
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
In your first example with an attractive blue car.
I still dont get why not just direct proof? The contradiction is just a layer around. You ended up concluding attractive(by modus ponens), only discharging your hypothetical at the very end
By a "direct proof" I'm guessing you mean some sort of Natural Deduction method? That's certainly possible, at least in this case, but that a different proof method than proof by contradiction, which is the method that all high-performance ATP systems use these days. Other styles of proof are easier to read but method of proof by contradiction are the fastest. If I'm misunderstanding your question though, I'd be eager for clarification.
@@adampease you know A
You know A=>B
Derive B
No need for contradicting a hypothetical?
@@nrrgrdn Indeed, for this simple problem it can be done with just one inference rule (and the resolution rule is a generalization)
@@adampease Resolution Theorem Proving, alright I get why it is efficient in general
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.
The python standard library unittest module is closely modeled after the respective Java framework.
Hello Prof. I want know is there any limitations of automated theorem prover?
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 ruclips.net/video/vre8CrPINrw/видео.html
@@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 👏👏👏🙏🙏👌👌
@@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