- Видео 89
- Просмотров 39 541
Ontology Talk with Adam Pease
Добавлен 23 ноя 2009
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
Neighborhood semantics in SUMO
A short explanation of the approach and interpretation to neighborhood semantics for reasoning with possible worlds in SUMO.
Просмотров: 152
Видео
Ontology of Coffee - Part II
Просмотров 462Год назад
For the second video in this series I concentrate more on the ontology and less on the espresso making process. I narrate the presentation of terms in SUMO that describe the objects and espresso making actions I'm taking in the video. You can explore the full definitions of each of the terms by typing them into the "KB term" field of the Sigma browser - sigma.ontologyportal.org:8443/sigma/Brows...
Espresso Ontology
Просмотров 319Год назад
I talk mostly about how I make a cappuccino at home but also show some of the terms from SUMO that can be used to describe the equipment and process Equipment (I may receive a small commission if you buy one of these) La Spaziale Mini Vivaldi II, Baratza Sette 270 - Clive Coffee is a good source pitcher - www.amazon.com/gp/product/B07RZSCVWS/ref=ppx_yo_dt_b_search_asin_title?ie=UTF8&psc=1&_enco...
A propositional logic proof with E
Просмотров 203Год назад
An example of an inference problem from the TPTP library. I show how to pose the problem to the E prover and give a quick explanation of the resulting proof and how to read it.
Different Logics
Просмотров 336Год назад
I give a few examples of different logical languages, their properties and an example inference using an automated theorem prover for each.
What Logic is needed to Represent Language?
Просмотров 292Год назад
I present a conference talk given previously on an experiment to show empirically what logic might be needed to capture the semantics of natural language.
Taming Digital Volatility
Просмотров 2932 года назад
Adam Pease speaks at the Next100 conference about how ontology can help manage the complexity of data.
SigmaNLP Part 2: A second demo with the NLP system built on SUMO and Stanford CoreNLP
Просмотров 1472 года назад
I provide another demo of the experimental SigmaNLP system showing how new concepts and lexical elements from the current pandemic can be used in language to logic translation
SigmaNLP: A brief introduction to an experimental NLP toolkit with SUMO
Просмотров 1782 года назад
I show a quick demo of an NLP toolkit for deep semantic understanding with SUMO. While experimental and flawed, it does show what may be possible in language to logic translation backed by a large ontology.
A SUMO Walkabout: Expressing a Situation Calculus Problem in SUMO
Просмотров 1662 года назад
I take an example inference problem that was the subject of an AI Journal article that was coded with the Situation Calculus and re-express it using SUMO. I also show the use of Vampire to do theorem proving with the resulting formalization.
Embedding SUMO in Set Theory
Просмотров 642 года назад
I talk about joint work with Chad Brown and Josef Urban to embed SUMO into higher order set theory. Our goal is to be able to reason with SUMO's higher order logic content and attempt to show that the HOL content doesn't have obvious logical inconsistencies.
OntologyTalk: An Interview with Dr. Chad Brown: Part 4
Просмотров 492 года назад
Chad talks about higher order theorem provers and recent advancements
OntologyTalk: An Interview with Dr. Chad Brown: Part 3
Просмотров 522 года назад
Chad talks about higher order set theory
OntologyTalk: An Interview with Dr. Chad Brown: Part 2
Просмотров 602 года назад
I interview Dr. Chad Brown about issues in Higher Order Logic
OntologyTalk: An Interview with Dr. Chad Brown, Part 1
Просмотров 1322 года назад
I interview Chad Brown about his work in higher order logic, including higher order theorem proving and set theory
Ontology Talk: Part 3: An interview with Prof. Christoph Benzmueller
Просмотров 1663 года назад
Ontology Talk: Part 3: An interview with Prof. Christoph Benzmueller
Ontology Talk: Part 2 of An Interview with Prof. Christoph Benzmueller
Просмотров 1293 года назад
Ontology Talk: Part 2 of An Interview with Prof. Christoph Benzmueller
Ontology Talk: An Interview with Prof. Christoph Benzmueller: Part 1
Просмотров 3303 года назад
Ontology Talk: An Interview with Prof. Christoph Benzmueller: Part 1
Ontology Talk: Formalizing "Shortage" in SUMO: Part2
Просмотров 1093 года назад
Ontology Talk: Formalizing "Shortage" in SUMO: Part2
Ontology Talk: Formalizing "Carabiner" in SUMO: Part 2
Просмотров 443 года назад
Ontology Talk: Formalizing "Carabiner" in SUMO: Part 2
Ontology Talk: Formalizing "Shortage" in SUMO
Просмотров 1023 года назад
Ontology Talk: Formalizing "Shortage" in SUMO
Ontology Talk: Formalizing "Carabiner" in SUMO
Просмотров 1103 года назад
Ontology Talk: Formalizing "Carabiner" in SUMO
Ontology Talk: Formalizing "Flight Attendant"
Просмотров 843 года назад
Ontology Talk: Formalizing "Flight Attendant"
Ontology Talk: Formalizing "Cruise Ship" in SUMO
Просмотров 883 года назад
Ontology Talk: Formalizing "Cruise Ship" in SUMO
Ontology Talk: Formalizing a New Concept in SUMO
Просмотров 903 года назад
Ontology Talk: Formalizing a New Concept in SUMO
Ontology Talk: Pre-processing SUMO for FOL
Просмотров 1013 года назад
Ontology Talk: Pre-processing SUMO for FOL
Ontology Talk: Negation by Failure: What to Answer when an AI doesn't Know for Sure
Просмотров 2413 года назад
Ontology Talk: Negation by Failure: What to Answer when an AI doesn't Know for Sure
Ontology Talk: An Interview with Dr. Lauri Karttunen: Part 2
Просмотров 543 года назад
Ontology Talk: An Interview with Dr. Lauri Karttunen: Part 2
Ontology Talk: An Interview with Prof. Lauri Karttunen
Просмотров 1743 года назад
Ontology Talk: An Interview with Prof. Lauri Karttunen
pardon a typo at 8:11 I start creating a quantifier list and then don't get back to doing it. Every quantifier needs a quantifier list such as with (exists (?T1 ?T2)... I also manage to misspell ascertain :-(
Great overview of the toolsets and their uses! Ties a lot together
Thanks! This one is getting a bit old but hopefully mostly still relevant. But now we have sigmanlp, sumonlp, SigmaUtils, SUMOjEdit in addition to sigmakee and sumo
I am rolling at the comment about coming back to your own code 5 years later... Great!
😀
I found this video to be very useful.
excellent! very glad to hear this. Please feel to ask any questions you might have too! These videos are also part of a free online course with exercises if you want to learn how to do formal ontology. If that interests you, please let me know and I'll send you a link
This was useful to me!
very glad to hear that!
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
Very cool! I saw sigma on the sumo website but it didn’t seem to be working at the time
thanks! Can you tell me what behavior you're getting from Sigma? It's working for me, for example, sigma.ontologyportal.org:8443/sigma/Browse.jsp?lang=EnglishLanguage&flang=SUO-KIF&kb=SUMO&term=ConstantQuantity
amazing. Thank you!
thanks! I'm always grateful for feedback, and eager to answer questions.
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 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
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/RUclips/SchulzNotes.pdf
Exciting!