CS4325 Ontology and Theorem Proving for Trusted Systems

Ontology, as taught in this course, is the discipline of creating a catalog of symbols and computable definitions of those symbols. It is an emerging area of computer science and is used in neuro-symbolic AI implementations and also in software engineering to ensure common human and machine understanding of data and meta-data. The Navy fields systems that have high trust and integration requirements. Ontology-based specification of data can create provably correct implementations. In addition, neurosymbolic approaches are being used to reduce hallucinations in machine learning applications and create explainable AI. This advanced course will be project based, aligning the students' interests or current research with the course content in ontology and theorem proving. There will be a mid-course and a final project submission. By the end of the course, each student should have the ability to model practical problems in first order and more expressive logics, using content that extends the Suggested Upper Merged Ontology (SUMO) and using the TPTPworld software and languages to perform logical inference with that content.

Prerequisite

Students need a basic foundation in logic which can be gained from CS3001

Lecture Hours

3

Lab Hours

2

Course Learning Outcomes

Students will have an understanding of different families of logical languages - propositional, description logic, first order logic, modal logic and higher order logic including the limitations and capabilities of each and how to apply them in a practical computational system on application projects. Students will be able to convert complex English sentences into an appropriate mathematical logic formula or formulas. Students will be able to code logical axioms in TPTP FOF, TPTP TFA and SUO-KIF. Students will be able to use the SystemOnTPTP, SigmaKEE and SUMOjEdit software to develop ontologies. Students will be able to use the Vampire theorem prover to ask queries on set of formulas.