ABSTRACT. 75 years after the birth of computing as a discipline with the founding of the Association for Computing Machinery, we seem to be witnessing a Kuhnian paradigm shift in computer science. The old paradigm of computer science as a science of formal models seems to be out, and a new paradigm of computer science as a data-driven discipline is in. I argue that the paradigm-shift paradigm has been overplayed. In reality, scientific paradigms glide rather than shift. Good old formal computer science is as important as ever. But there has been a paradigm shift in how computing research is being carried out. The center of gravity in computing research used to be in academia, where its goal was to contribute to the common good. Today this center of gravity moved to industry, where its goal is to maximize corporate profits.

ABSTRACT. Coding agents such as Claude Code, Codex and others are creating a new paradigm that will change programming in ways impossible to foresee. Recent experiences with coding agents indicate that they can easily generate logic programs in Prolog and ErgoAI, as well as lower-level Prolog system code. We conjecture about the implications of these experiences and suggest research pathways to explore the importance of logic programs can in an age of coding agents.

ABSTRACT. Anil Nerode is Goldwin Smith Professor of Mathematics and Computer Science at Cornell University. He is “a pioneer in mathematical logic, computability, automata theory, and the understanding of computable processes, both theoretical and practical for over half a century, whose work comes from a venerable and distinguished mathematical tradition combined with the newest developments in computing and technology.”

ABSTRACT. We posit that prior and ongoing work on hidden layer neuron analysis gives rise to a neurosymbolic approach to improved cyber-physical systems control via a runtime monitoring system that combines deep neural networks and formal reasoning over knowledge graphs. Such a system would continuously observe neuron activation states (interpreted via neuron labels as system perceptions), assess whether the system perceptions are compatible with actual sensor readings, and suppress system control actions that are deemed as likely mispredictions.

ABSTRACT. Data-centric AI, exemplified by the rapid advancement of deep learning and large language models, has fueled discussions of Artificial General Intelligence. However, for scientific discovery and high-stakes decision-making, purely data-driven methods face significant limitations. These include opaque behavior with limited interpretability, restricted use of prior knowledge, and brittle performance outside the training distribution. Furthermore, these models often struggle with heavy data requirements and complex multi-objective trade-offs. I discuss a knowledge-centric AI agenda designed to overcome these hurdles. This approach combines first-principles reasoning with data-driven learning, integrating prior scientific knowledge with data to produce interpretable and informed recommendations. I will discuss recent work in computational sustainability, highlighting how this framework facilitates discovery, prediction, and decision-making in high-stakes environments.

ABSTRACT. What do query processing, deep learning and quantum computing have in common? They can be formulated and generalized as dealing with linear operators over spaces such as free (semi)modules and Hilbert spaces, with associated classical algebras such as Boolean, associative and tensor algebras. The algebras have universal equational properties that can be exploited at run time by judicious simplification. Part of the trick is resisting the temptation to normalize data to a normal form, but employing symbolic operators that not only delay evaluation (as in lazy evaluation), but act differently depending on the context in which they occur at run time. The challenge then is when and how much to simplify, which data structures to use, and how to analyze the algorithmic consequences. We illustrate this methodology by applying it to * relational first-order logic based query evaluation, where we show that it is easy to program worst-case optimal joins on in-memory data that are secure against algorithmic complexity attacks, require few lines of code in Python or Haskell and perform quite well compared to even highly advanced and mature query compilers and database systems; * automatic differentiation (AD), where it leads to a DSL for compactly representing linear operators and computing their adjoints for reverse-mode AD. We will hint at other applications that we have developed in this fashion, from quantum circuit simulation to greenwashing-proof virtual energy sourcing. And we will encourage participants to think of more cases where this may be a (potentially revisionist) way of formulating their underlying methodology

ABSTRACT. Trustworthy AI in the legal domain can be achieved using reasoning-based expert systems. Furthermore, usability and performance of such systems can be improved by using generative AI and adding a human-verification step of generative AI's output-preserving trustworthiness. In addition, the common pitfall of automation bias can be avoided if verification becomes unavoidable and avoidance becomes equivalent to output refutation. We describe a system that demonstrates these claims in practice. By grounding its reasoning in a manually-created Datalog knowledge base with schematic natural-language translations, using an LLM to bridge the gap between natural language case descriptions and Datalog facts, and requiring each generated fact to be human-verified, the system achieves greater usability without compromising on trustworthiness.

ABSTRACT. Abstract: Human-AI Communication for Deontic Reasoning Devops (CODORD) intends to create new, automated techniques for humans to author knowledge about deontics (obligations, permissions, and prohibitions) into an expressively flexible logical language by using natural language (i.e., English). CODORD has the potential to enable automated deontic reasoning with high assurance (i.e., verifiability/explainability and correctness) to assess compliance with orders, regulations, laws, operational policies, and ethics.

ABSTRACT. The Compositional Learning-And-Reasoning for AI Complex Systems Engineering (CLARA) fundamental research program is designed to tightly integrate Automated Reasoning (AR) and Machine Learning (ML) components to create high-assurance AI — which is expected to scale even to complex systems of systems. Integrating the two different branches of AI will provide the speed and flexibility of ML with verifiability based on AR proofs that have strong logical explainability and computational tractability.