Ontology Talk with Adam Pease
Ontology Talk with Adam Pease
Talks about ontology in computer science, applications of ontology, Artificial Intelligence and knowledge representation. Discusses the details of the Suggested Upper Merged Ontology (SUMO) and its Sigma tool set - www.ontologyportal.org
Пікірлер
Thank you for making this video @adam. I may have to look up to your earlier work to see how to get to this collection of logic formulae.
Glad you liked it and eager to be of help. All the formulas are available at github.com/ontologyportal/sumo
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!
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 kzread.info/dash/bejne/qKaZmqWrgKy0oto.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
you'll also need to assert that (instance X Object) , (instance Y Object) , (instance Z Object) apologies for the omission
Now you’re responsible for me having a too-early flat white 😊 Nice set up - will need to negotiate some extra counter space at home.
Once i got good coffee equipment I was hooked :-)
Very interesting approach for introduction to ontology development.
Thanks John!
Love this! Thank you Adam
3:04 propositional logic 9:44 description logic 12:44 first-order form 18:56 typed first-order form with arithmetic 24:09 typed higher-order form
Thanks! Very helpful
You can get Eprover at github.com/eprover/eprover , Vampire at github.com/vprover/vampire and LEO-III at github.com/leoprover/Leo-III . Problems here are taken from www.tptp.org/
I was surprised to hear the claim that no large investment in formalizing knowledge and using theorem-proving had ever been attempted, because Doug Lenat's CYC was such a project for more than 20 years.
I don't recall Chris saying that. He's aware of both SUMO and Cyc, which fit that description. What time point in the video?
I might be misinterpreting but he says it might be time for a big investment at 14:00 and later says there's never been one.
Also, I just came across this channel and your papers. It would be very interesting to watch a talk about theorem-proving with epistemic inferences about BDI situations. Like you say at pne point in your natural language talk, there is very little about this published that is digestible by non-experts.
@@DavidP-um6mg I will shortly post an overview of different logics on this channel. At lot more detail is needed and I hope to do more.
@@DavidP-um6mg yes, you have to listen to his entire (rather long) sentence where he says that it's time for a major investment in theorem proving with logical pluralism (not just one company with a proprietary implementation)
I did everyhting as in video but in the end stuck with BUILD FAILED /home/theuser/workspace/sigmakee/build.xml:42: The following error occurred while executing this line: Error reading project file /home/theuser/workspace/TPTP-ANTLR/build.xml: /home/theuser/workspace/TPTP-ANTLR/build.xml
Do you have a user "theuser"? What do you get if your run "ls -la /home/theuser/workspace/sigmakee". It looks like you need to fix your paths in your SIGMA_SRC environment variable, as specified in the install instructions. I'm glad to do a video call with you to help with the install if that doesn't solve it for you.
sorry for the lack of audio, I need to redo this old video. Some useful visuals, showing higher order operators in the Sigma browser, begin at 2:30
Re "many Esquimaux terms for 'snow:'" The first European source who reported this, counted as separate terms universally-differentiated distinctions among physical referents in the Inuit languages: "This snow beside me," "The snowfall last year that you just mentioned..." are distinguished exactly as are "This gutting-blade I'm holding" versus "The consignment of gutting blades that you bought a while ago and are talking about." As you hinted: Counted rationally, professional European skiers have quite a lot more names for "actionably distinct kinds of snow" than do traditional Inuit. Source: MAK Halliday, University of Illinois lecture, 1976, on "Fallacies in 'Sapir-Whorf.'"
That's great detail Dave, thanks!
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
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
👍🇦🇷🌎
Thank you for a well rounded overview of the topic: neither oversimplistic nor overcomplicated!
Many thanks for the feedback! I hope that you may find some of my other videos helpful too. I'm always glad to answer questions.
hi, could you make a video on building sigmanlp? I am having some difficulties
Hi Jeferson, you're welcome to email me and I'm glad to help. Just let me know where in the installation instructions you're having trouble and what errors messages you get
p̲r̲o̲m̲o̲s̲m̲
Thank you for the video!
This is not Chad.
just his body double :-)
Hi Professor Adam, I have a question about the instances, can a ontology contain a lot of instances? And how can we connect those intances within a ontology? For example, we have thress persons, there belong to class "Person", but all of them have two hands, we have also a class "Hand" and 6 hand instances, e.g. hand1, hand2, hand3, hand4, hand5 and hand6, how can specify the connection of those instances within ontology? Person1 has hand1 and hand2 like that. Thanks and best regards. Ryan.
Yes, an ontology can have many instances. Look at sigma.ontologyportal.org:8443/sigma/Browse.jsp?kb=SUMO&lang=EnglishLanguage&flang=SUO-KIF&term=Nation and you'll see many Nations of the world, which also have facts such as their geographical relationship to each other. To specify that one person named "John" has two particular hands, we would state (and (instance Hand1 Hand) (instance Hand2 Hand) (not (equal Hand1 Hand2) (part Hand1 John) (part Hand2 John) (instance John Human) (names "John" John)). Similarly, you could define two other people and their hands, being careful to say they are all not equal to each other.
Which is the right order of the activities for the development of ontologies ? A. Specification , Formalisation, Conceptualisation, Implementation B. Specification , Conceptualisation, Formalisation ,Implementation C. Conceptualisation, Specification, Formalisation ,Implementation D. Formalisation ,Specification , Conceptualisation, Implementation
I recommend the process at ontologyportal.org/Process.html
Activities such as ontology merging and ontology alignment is part of which step during the knowledge acquisition phase : A. Extraction B. Evaluation C. Integration D. Configuration Management
It depends on the ontologies you are using. Many things that are called ontologies don't have the formal definitions that SUMO does, so the first step is to determine the meaning of the terms that you want to integrate with SUMO, even informally as a dictionary definition. Then determine which of them SUMO already covers, or which can't be defined and should be discarded. A good case study and overview is www.semantic-web-journal.net/system/files/swj2520.pdf
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.
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
Great video. Could you give an example of inference using this definition?
Many of the axioms are HOL, but fortunately a couple are FOL. We could say "John has a shortage of 5 apples on Tuesday for $1." If we then assert that "John bought 5 apples on Tuesday for $1." we'll have a contradiction
Awesome video!
thanks!
Prof Benzmuller is amazing! He is so at ease discussing these complex concepts of and different branches in logic and with Clarity. It is a breeze what this interview. Thank you!
Indeed it is an honor to have been able to interview him
Indeed, this seems like a very sophisticated relation to formalise. Your two-part video on how to formalise this concept of shortage may conceivably be used as a comprehensive training material which covers the fundamental concepts which run across the 7 of the 11 modules in SUMO: Set/Class Theory, Numeric, Temporal, Measure, Processes, Objects and Quantities listed out in your book. facebook.com/Ontology-A-Practical-Guide-285988794762942
So glad that you found this informative!
Thank you for walking us through the thinking and coding processes of how to formalise a "Relation" in SUMO. It is very helpful. Question 1: How do you distinguish between a scarcity and a shortage of a certain class of object. For example, I am thinking of a natural resource such as water. It is in some sense "free" goods. Is cost/price always necessary in this kind of goods?
Excellent question! If it's really free then there's no shortage. One might have a glacial stream in the back yard that flows year-round and you get all your water from that. Then there's no shortage. But if you live in a city, water may appear plentiful but you pay a fee each month (probably both a connection fee or minimum and a per-quantity rate), so in that case the water has a specific cost, and so there is a shortage at any lower cost. In the western US many places have water restrictions this summer so there's an explicit shortage. You could buy a big tank (if you have space and own your home, and which has a cost) and pay to have a tanker truck deliver water (probably at a much higher cost), so in that case there's more clearly a shortage.
Great demonstration, Adam!
thanks!
I had a problem using the login page with Tomcat that I resolved by using the manager webapp and adding the sigma webapp
Interesting! Tomcat should recognize the presence of any new .jar file in the webapps directory upon restart. Feel free to email me if you need any further help.
Very clear explanation, Adam! Thank you for sharing.
Thanks! I hope you enjoy some of my other ontology videos as well.
References to things mentioned - E prover - eprover.org leanCoP - www.leancop.de/ Gradient boosted trees - en.wikipedia.org/wiki/Gradient_boosting Mizar - mizar.org/ Fermat's last theorem - en.wikipedia.org/wiki/Fermat%27s_Last_Theorem Kepler Conjecture , solved by Toth and Hales - en.wikipedia.org/wiki/Kepler_conjecture Cezary Kaliszyk - cl-informatik.uibk.ac.at/users/cek/ Stephan Schulz - wwwlehre.dhbw-stuttgart.de/~sschulz/DHBW_Stephan_Schulz/Stephan_Schulz.html arity - en.wikipedia.org/wiki/Arity De Morgan's Law - en.wikipedia.org/wiki/De_Morgan%27s_laws Tribolet - ??? Office of Naval Research - www.onr.navy.mil/ Dana Scott continuous Lattices - www.cs.ox.ac.uk/files/3229/PRG07.pdf first order logic - en.wikipedia.org/wiki/First-order_logic set theory - en.wikipedia.org/wiki/Set_theory TPTP - tptp.org Christian Szegedy - scholar.google.com/citations?user=3QeF7mAAAAAJ&hl=en System 1 and 2 - suebehaviouraldesign.com/kahneman-fast-slow-thinking/ Roger Penrose - en.wikipedia.org/wiki/Roger_Penrose Srinivasa Ramanujan - blog.sciencemuseum.org.uk/instinct-intuition-and-mathematics-the-divine-genius-of-srinivasa-ramanujan/ Max Planck - en.wikipedia.org/wiki/Max_Planck John Harrison - www.cl.cam.ac.uk/~jrh13/ Byron Cooke ? DARPA - www.darpa.mil/ Mike Douglas - scgp.stonybrook.edu/people/faculty/bios/michael-r-douglas Bacon System ? Kryštof Hoder - www.linkedin.com/in/krystof/ SInE - SUMO Inference Engine - www.cs.man.ac.uk/~hoderk/sine/
References for this and later parts of the interview - E prover - eprover.org Our ENIGMA 70% improvement: doi.org/10.4230/LIPIcs.ITP.2019.34 ATP Proofs of 74% of Mizar (thanks mainly to ENIGMA): github.com/ai4reason/ATP_Proofs/blob/master/README.md leanCoP - www.leancop.de/ Gradient boosted trees - en.wikipedia.org/wiki/Gradient_boosting Our “AlphaZero” for leanCop (rlCoP): papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving Mizar - mizar.org/ Fermat's last theorem - en.wikipedia.org/wiki/Fermat%27s_Last_Theorem Kepler Conjecture, proved by Hales and Ferguson, see en.wikipedia.org/wiki/Kepler_conjecture#Hales'_proof Cezary Kaliszyk - cl-informatik.uibk.ac.at/users/cek/ Stephan Schulz - wwwlehre.dhbw-stuttgart.de/~sschulz/DHBW_Stephan_Schulz/Stephan_Schulz.html arity - en.wikipedia.org/wiki/Arity De Morgan's Law - en.wikipedia.org/wiki/De_Morgan%27s_laws Andrzej Trybulec - en.wikipedia.org/wiki/Andrzej_Trybulec Office of Naval Research - www.onr.navy.mil/ Dana Scott continuous Lattices - the book formalized in Mizar is www.amazon.com/Compendium-Continuous-Lattices-G-Gierz/dp/3642676804 first order logic - en.wikipedia.org/wiki/First-order_logic set theory - en.wikipedia.org/wiki/Set_theory TPTP - tptp.org Christian Szegedy - scholar.google.com/citations?user=3QeF7mAAAAAJ&hl=en System 1 and 2 - suebehaviouraldesign.com/kahneman-fast-slow-thinking/ Roger Penrose - en.wikipedia.org/wiki/Roger_Penrose Srinivasa Ramanujan - blog.sciencemuseum.org.uk/instinct-intuition-and-mathematics-the-divine-genius-of-srinivasa-ramanujan/ Max Planck - en.wikipedia.org/wiki/Max_Planck John Harrison - www.cl.cam.ac.uk/~jrh13/ Byron Cooke - www0.cs.ucl.ac.uk/staff/b.cook/ DARPA - www.darpa.mil/ Mike Douglas - scgp.stonybrook.edu/people/faculty/bios/michael-r-douglas Bacon System - dl.acm.org/doi/10.5555/1624861.1624976 , link.springer.com/chapter/10.1007/978-3-662-12405-5_10 Kryštof Hoder - www.linkedin.com/in/krystof/ SInE - SUMO Inference Engine - www.cs.man.ac.uk/~hoderk/sine/
pardon the error at about 8:00 - 9pm is 21:00 hours on a 24-hour clock
Onward! - Into the Adjacent Possible!
ontology is all about encoding what's possible to encode, so... sure!
AI Index report mentioned in the interview - aiindex.stanford.edu/wp-content/uploads/2021/03/2021-AI-Index-Report_Master.pdf
Thank you.
Notes and references are available at www.articulatesoftware.com/KZread/SchulzNotes.pdf
Exciting!
Thanks, Adam! Ai should be explainable, but that doesn't mean dumping all of the guts of an AI application on the user. Thoughtful HCI is an important component of AI implementation.
Agreed!
A video that includes discussion of how to use a truth table to prove the validity of a logic transformation is kzread.info/dash/bejne/m5ehy9WQpbCad7w.html&ab_channel=AdamPease
A transcript and study guide for parts 1 and 2 of this short series is at www.adampease.org/OP/paraphrasingLogic.pdf . Part 1 is at kzread.info/dash/bejne/faCLzMWuc7OfdtI.html
A document with much of the content of the video is at www.adampease.org/OP/paraphrasingLogic.pdf
Hello Mr. Pease. I am attempting to email you at [email protected], but infosys informs me that this email is unavailable. Can I reach you at another address?
I've moved on from Infosys and am back to Articulate Software. My email is in the first slide for this video :-)
@@adampease oh, derp. many thanks. i'll email shortly.
Part 1 of this series is kzread.info/dash/bejne/c6iNq8aLZ9q-qs4.html
Thanks Adam. I didn’t realize Ontology could be applied to AB tests as well. If possible, please do more of ontology application videos as they really help folks not closely related to the field understand the use cases.
thanks! will do!
I have often informally made the 'variable substitution' argument to point out that a lot of what we see as intelligent behavior in a formal system is really just parasitic on the meanings 'in our head', but this is the first time I see it laid out so well in a presentation!