Automating Argumentation (for Overarching Properties) with Goal-directed Answer Set Programming

Presented as part of the 2021 HCSS conference. 

ABSTRACT

Formalizing the human thought process has been considered very difficult. The field of informal logic has been developed in recognition of this difficulty where an argument is interpreted as an attempt to present evidence for a conclusion. Holloway and Wasson have developed a primer to establish the terms, concepts, principles, and uses of arguments to reason about overarching properties [4]. We argue that recent advances in automated reasoning, especially incorporation of negation as failure (NAF), facilitate the formalization of the human thought process. These advances help formalize concepts that were hitherto thought of as impossible to formalize. We show how the paradigm of answer set programming (ASP), that incorporates NAF, can be used to formalize all the concepts presented in Holloway and Wasson’s primer on argument. The main application of our work is in automated software systems certification and assurance. The goal is to represent the thought process of a human software certifier using ASP. ASP has been shown to be a highly suitable paradigm for knowledge representation and reasoning. It has been applied to many intelligent tasks including visual and natural language question answering [2] and emulating advanced human expertise (where it can outperform the human expert) [3].

In the overarching properties method, a human certifier starts with the goal of establishing intent, correctness and innocuity. Next, the certifier will have to construct arguments to prove these goals. An example argument maybe the following: a software is correct, if each of its components are correct and all interactions between the components are correct. Arguments will have to be made recursively then to establish the correctness of each component/interaction. Eventually, this chain of argument ends in a belief where a belief could be based on hard evidence (fact) or an assumption. Arguments may also be defeated: a defeater provides support for not believing an argument. Thus, we use reasoning process that reaches a conclusion using arguments and beliefs. We show how a conclusion can be mapped to an ASP query, an argument to an ASP rule, an evidence to an ASP fact, an assumption to an abducible, and a defeater to a negated goal. An argument thus can be coded in ASP and the resulting program can be run on our goal-directed s(CASP) system [1] to automatically establish a conclusion in presence of evidence, assumptions and defeaters. In the talk we will present our general methodology and illustrate it with several non-trivial examples.

References

1. Joaqu´ın Arias, Manuel Carro, Elmer Salazar, Kyle Marple & Gopal Gupta (2018): Constraint answer set programming without grounding. TPLP 18(3-4), pp. 337–354.
2. Kinjal Basu, Sarat Chandra Varanasi, Farhad Shakerin, Joaquin Arias & Gopal Gupta: Knowledge driven Natural Language Understanding of English Text and its Applications. In: Proc. of AAAI 2021.
3. Zhuo Chen, Elmer Salzar & Others (2018): An AI-Based Heart Failure Treatment Adviser System. IEEE journal of translational engineering in health and medicine 6, 2800810.
4. C. Michael Holloway & Kimberly S. Wasson (2020): A Primer on Argument. Available at https://shemesh.larc.nasa.gov/people/cmh/cmhpubs.html.

Gopal Gupta is a professor of computer science at the University of Texas at Dallas where he holds the Erik Jonsson chair.  His areas of research interest are in automated reasoning, logic programming, machine learning, programming languages, and assistive technology. He has published extensively in these areas. His group has also authored many software systems, many of which are publicly available. His research work has also resulted in commercial software systems that have formed the basis of two startup companies.  His group has won several best-paper awards as well as the ICLP 2016 most influential paper award for their work on co-inductive logic programming. Prof. Gupta's current research is funded by the NSF and DARPA. His lab is one of nine labs worldwide currently competing in the Amazon Alexa Socialbot competition where the goal is to build an Alexa skill that can hold a casual conversation with a random user for at least 20 minutes. He obtained his MS & PhD degrees from UNC Chapel Hill and his B.Tech. in Computer Science from IIT Kanpur, India. 

Kinjal Basu is a computer science Ph.D. student working under Prof. Gopal Gupta on closed domain question-answering and commonsense reasoning. Currently, he is leading the CASPR team from UT Dallas at the 'Alexa Prize: Social Bot Grand Challenge 4' competition organized by Amazon. His research interest lies in Logic Programming, Natural Language Understanding, and Machine Learning, and his recent papers are in the area of textual and visual question answering and conversational agents. Kinjal also acquired real-world data science project experience while working as an intern at Intuit. During his Bachelor's in Information Technology, he worked on several NLP projects (e.g., Text Similarity) and also interned at IIT Kharagpur for NLP research.

Zhuo Chen’s Ph.D. work focused on the development of a system for recommending heart failure treatment based on automating commonsense reasoning with answer set programming. The system was developed in collaboration with cardiologists. He subsequently worked as a postdoctoral researcher at the University of Texas at Dallas where he continued his work on automation of commonsense reasoning.  In the past, Zhuo has also worked in mission-critical software system development and implementation. Aside from Answer Set Programming, Zhuo also enjoys programming in Scala and Go and currently works as a backend developer for Kinzoo.

Elmer Salazar is an assistant professor of instruction at the University of Texas at Dallas. Though teaching full time, he dedicates time to research, and works with the ALPS research group. His research interests include non-monotonic computational logic, the application of computational logic to AI and common sense reasoning, and the interaction of machine learning techniques (neural networks) and computational logic. He is the co-designer of the s(ASP) language (a non-monotonic, ungrounded, goal-directed logic programming language based on stable model semantics), and recently has been working on using proof trees generated by proof-theoretic execution to automatically find possible problems in ASP code based on some requirements encoded as predicates.

Farhad Shakerin is an experienced software engineer from the railway signaling industry. He contributed to the development of safety-critical systems for ten years before joining the graduate program at The University of Texas at Dallas. In 2020, he received a Ph.D. degree in Computer Science. His dissertation contributed to the field of explainable AI and logic-based natural language understanding. He is currently a senior software engineer at Microsoft Azure Cognitive Service.

Serdar Erbatur is an assistant professor of instruction at UT Dallas. He received his PhD degree from University at Albany (SUNY) in 2012. He has held postdoc positions in University of Verona (Italy), LMU Munich (Germany) and IMDEA Software Institute (Spain). He also visited INRIA Nancy (France) and Technical University of Valencia (Spain) for short terms. His current research is centered on automated reasoning and type-based program analysis with the overarching goal of applying it to formal verification (of programs and protocols). Currently, he is working on two ongoing research projects; (i) logical problems for protocol verification and (ii) the GuideForce project, funded by the German Research Foundation, focused on developing a program analysis tool for checking if a given Java program follows desired best programming practices (guidelines).

Fang is a Computer Science PhD candidate in Prof. Gopal Gupta’s lab. Fang's research interests are explainable AI, commonsense reasoning, answer set programming, and logic programming. Fang got his Master' in Applied Mathematics & Computer Science and graduated with honors from University of Central Oklahoma. In the past few years he has conducted research on human computer interaction, IoT, autonomous vehicles, AI planning, and answer set programming implementation. He cofounded a company as a CTO called Turning Systems that won an award in an entrepreneurship competition.

Huaduo Wang is a PhD student in the ALPS lab led by Prof. Gopal Gupta. His current research focus on textual based QA, commonsense reasoning. His research interest lies in logic programming, natural language processing and understanding. His past work and research experience were in computer systems, distributed systems and autonomous vehicles. For his Master’s research, he worked on system kernel project. He has interned as a backend SDE at Baidu as well as worked as a full-time software engineer for 3 years in the banking industry.

Joaquín Arias is an assistant professor at Universidad Rey Juan Carlos in Madrid (URJC). He obtained his M.Arch. in Architecture in 2002, his B.Sc./M.Sc. degrees in Informatics in 2014/2015, and received a Ph.D. in Computer Science in 2020, from the Universidad Politécnica de Madrid. His principal area of expertise is the development and application of advanced evaluation techniques for (non-)monotonic reasoning using rules and constraints. His background includes the implementation of an abstract interpreter based on tabled constraint logic programming, and the development (in collaboration with the IMDEA Software Institute and the University of Texas at Dallas) of s(CASP) a novel non-monotonic reasoner that evaluates constraint answer set programs. He is currently a fellow of the Artificial Intelligence Research Group at the URJC and his research interests are in the areas of Event Calculus, XAI, and Building Information Modeling.

Brendan Hall is an Engineer Fellow with Honeywell Aerospace Advanced Technology. He has over 25 years of experience within safety-relevant domains and has successfully executed internal and externally funded (NASA, AFRL, and FAA) research programs. His research interests include fault-tolerant distributed system architectures, model-based system and safety engineering, formal and property-based design assurance, and the industrial application of formal methods and logic programming. Mr. Hall holds over 45 patents and has published numerous technical papers within the fields of fault-tolerant distributed systems, requirement engineering, applied formal methods, and model-based engineering. 

Kevin Driscoll is a Fellow at Honeywell Labs with 49 years' experience in safety and security critical systems -- including the aspects of hardware, software, and system design.  He currently is leading an $8M effort to create assurance cases.  Other recent programs include "Considerations in Assuring Safety of Increasingly Autonomous Systems", "Validation and Verification of Safety-Critical Integrated Distributed Systems", and "Cyber Safety and Security for Reduced Crew Operations".  He was a main author of several embedded system network standards and the FAA network selection handbook.  Kevin is a consultant to other Honeywell divisions for dependable computing, electronic architectures, and data networks.  Kevin has over 50 patents and numerous publications covering safety and security critical real-time systems.