ACM fellow Dana Stewart Scott, the recipient jointly with Michael Rabin of the 1976 A.M. Turing Award for the concept of nondeterministic finite automata, has made seminal contributions spanning computing science, mathematics, philosophy, automata theory, modal logic, model theory, set theory, and the theory of programming languages. After receiving a B.A. in mathematics from the University of California, Berkeley, in 1950, and a Ph.D. from Princeton University in 1958, he held faculty positions at the University of Chicago, UC Berkeley, and at Stanford, Princeton, Oxford, and Carnegie Mellon Universities. He retired as University Professor from CMU in 2003. The distinguished theoretical computer scientist Gordon Plotkin conducted a series of four oral history interviews of Scott between November 2020 and February 2021. The interviews, the transcripts and videos of which are online,a cover primarily the period leading up to the 1976 ACM A.M. Turing Award. Presented here is a condensed and highly edited version, which includes some additional post-interview material provided by Scott. I was born in 1932 in Berkeley, CA, where I am now in retirement. We lived on a farm near Susanville when I started first grade in a one-room school-house.

We study the computational complexity of abstract argumentation semantics based on  weak admissibility, a recently introduced concept to deal with arguments of self-defeating  nature. Our results reveal that semantics based on weak admissibility are of much higher  complexity (under typical assumptions) compared to all argumentation semantics which  have been analysed in terms of complexity so far. In fact, we show PSPACE-completeness  of all non-trivial standard decision problems for weak-admissible based semantics. We then  investigate potential tractable fragments and show that restricting the frameworks under  consideration to certain graph-classes significantly reduces the complexity. We also show  that weak-admissibility based extensions can be computed by dividing the given graph into  its strongly connected components (SCCs). This technique ensures that the bottleneck  when computing extensions is the size of the largest SCC instead of the size of the graph  itself and therefore contributes to the search for fixed-parameter tractable implementations  for reasoning with weak admissibility. 

As we grant artificial intelligence increasing power and independence in contexts like healthcare, policing, and driving, AI faces moral dilemmas but lacks the tools to solve them. Warnings from regulators, philosophers, and computer scientists about the dangers of unethical artificial intelligence have spurred interest in automated ethics--i.e., the development of machines that can perform ethical reasoning. However, prior work in automated ethics rarely engages with philosophical literature. Philosophers have spent centuries debating moral dilemmas so automated ethics will be most nuanced, consistent, and reliable when it draws on philosophical literature. In this paper, I present an implementation of automated Kantian ethics that is faithful to the Kantian philosophical tradition. I formalize Kant's categorical imperative in Dyadic Deontic Logic, implement this formalization in the Isabelle/HOL theorem prover, and develop a testing framework to evaluate how well my implementation coheres with expected properties of Kantian ethic. My system is an early step towards philosophically mature ethical AI agents and it can make nuanced judgements in complex ethical dilemmas because it is grounded in philosophical literature. Because I use an interactive theorem prover, my system's judgements are explainable.

CD Tools is a Prolog library for experimenting with condensed detachment in first-order ATP, which puts a recent formal view centered around proof structures into practice. From the viewpoint of first-order ATP, condensed detachment offers a setting that is relatively simple but with essential features and serious applications, making it attractive as a basis for developing and evaluating novel techniques. CD Tools includes specialized provers based on the enumeration of proof structures. We focus here on one of these, SGCD, which permits to blend goal- and axiom-driven proof search in particularly flexible ways. In purely goal-driven configurations it acts similarly to a prover of the clausal tableaux or connection method family. In blended configurations its performance is much stronger, close to state-of-the-art provers, while emitting relatively short proofs. Experiments show characteristics and application possibilities of the structure generating approach realized by that prover. For a historic problem often studied in ATP it produced a new proof that is much shorter than any known one.

In this paper, we apply incremental answer set solving to product configuration. Incremental answer set solving is a step-wise incremental approach to Answer Set Programming (ASP). We demonstrate how to use this technique to solve product configurations problems incrementally. Every step of the incremental solving process corresponds to a predefined configuration action. Using complex domain-specific configuration actions makes it possible to tightly control the level of non-determinism and performance of the solving process. We show applications of this technique for reasoning about product configuration, like simulating the behavior of a deterministic configuration algorithm and describing user actions.

Theory of stable models is the mathematical basis of answer set programming. Several results in that theory refer to the concept of the positive dependency graph of a logic program. We describe a modification of that concept and show that the new understanding of positive dependency makes it possible to strengthen some of these results.

Over the last decade, Neural Networks (NNs) have been widely used in numerous applications including safety-critical ones such as autonomous systems. Despite their emerging adoption, it is well known that NNs are susceptible to Adversarial Attacks. Hence, it is highly important to provide guarantees that such systems work correctly. To remedy these issues we introduce a framework for repairing unsafe NNs w.r.t. safety specification, that is by utilizing satisfiability modulo theories (SMT) solvers. Our method is able to search for a new, safe NN representation, by modifying only a few of its weight values. In addition, our technique attempts to maximize the similarity to original network with regard to its decision boundaries. We perform extensive experiments which demonstrate the capability of our proposed framework to yield safe NNs w.r.t. the Adversarial Robustness property, with only a mild loss of accuracy (in terms of similarity). Moreover, we compare our method with a naive baseline to empirically prove its effectiveness. To conclude, we provide an algorithm to automatically repair NNs given safety properties, and suggest a few heuristics to improve its computational performance. Currently, by following this approach we are capable of producing small-sized (i.e., with up to few hundreds of parameters) correct NNs, composed of the piecewise linear ReLU activation function. Nevertheless, our framework is general in the sense that it can synthesize NNs w.r.t. any decidable fragment of first-order logic specification.

As pointed out by [Davis and Marcus, 2015], 'Actions' play a vital role in how humans interact imagine a guest asks a robot for a glass of wine; if the robot with the world and enable them to achieve desired sees that the glass is broken or has a dead cockroach inside, it goals. As a result, most common sense (CS) knowledge should not pour the wine and serve it. Similarly, if a cat runs for humans revolves around actions. While in front of a house-cleaning robot, the robot should neither'Reasoning about Actions & Change' (RAC) has run it over nor sweep it up nor put it away on a shelf. Hence, been widely studied in the Knowledge Representation the ability of artificial agents to perform reasoning and integrate community, it has recently piqued the interest CS knowledge about actions is highly desirable.

This paper considers the problem of characterizing the stability region of a large-scale networked system comprised of dissipative nonlinear subsystems, in a distributed and computationally tractable way. One standard approach to estimate the stability region of a general nonlinear system is to first find a Lyapunov function for the system and characterize its region of attraction as the stability region. However, classical approaches, such as sum-of-squares methods and quadratic approximation, for finding a Lyapunov function either do not scale to large systems or give very conservative estimates for the stability region. In this context, we propose a new distributed learning based approach by exploiting the dissipativity structure of the subsystems. Our approach has two parts: the first part is a distributed approach to learn the storage functions (similar to the Lyapunov functions) for all the subsystems, and the second part is a distributed optimization approach to find the Lyapunov function for the networked system using the learned storage functions of the subsystems. We demonstrate the superior performance of our proposed approach through extensive case studies in microgrid networks.

Teaching a deep reinforcement learning (RL) agent to follow instructions in multi-task environments is a challenging problem. We consider that user defines every task by a linear temporal logic (LTL) formula. However, some causal dependencies in complex environments may be unknown to the user in advance. Hence, when human user is specifying instructions, the robot cannot solve the tasks by simply following the given instructions. In this work, we propose a hierarchical reinforcement learning (HRL) framework in which a symbolic transition model is learned to efficiently produce high-level plans that can guide the agent efficiently solve different tasks. Specifically, the symbolic transition model is learned by inductive logic programming (ILP) to capture logic rules of state transitions. By planning over the product of the symbolic transition model and the automaton derived from the LTL formula, the agent can resolve causal dependencies and break a causally complex problem down into a sequence of simpler low-level sub-tasks. We evaluate the proposed framework on three environments in both discrete and continuous domains, showing advantages over previous representative methods.