Finite automata are one of the most fundamental models of computation and are taught in almost all undergraduate computer-science curricula. Although automata are typically presented as a theoretical model of computation, they have found their place in a variety of practical applications, such as natural language processing, networking, program verification, and regular-expression matching.

We have a serious problem with how we have been teaching computability theory, a central component of the ACM/IEEE computer science curriculum. For a fair number of years, I taught a computability course.

A team of researchers has completed the understanding of the Keller Conjecture, first proposed in 1930, about the packing of squares, cubes, and their higher-dimensional analogues. The conjecture states that any tiling of identical hypercubes that fills space must contain a pair of neighbors that share an entire face. You might convince yourself it is true for two or three dimensions by toying with squares or blocks. Mathematicians later established the status of the conjecture for all dimensions except seven. The new result, which shared the best paper award at the 2020 International Joint Conference on Automated Reasoning (IJCAR 2020), fills that gap.

Non-monotonic reasoning is an essential part of human intelligence prominently formalized in artificial intelligence research via answer set programming. Describing complex objects as the composition of elementary ones is a common strategy in computer science and science in general. This paper contributes to the foundations of answer set programming and artificial intelligence by introducing and studying the sequential composition of answer set programs. Specifically, we show that the notion of composition gives rise to a family of finite monoids and seminearrings, baptized {\em ASP monoids} and {\em ASP seminearrings} in this paper. Particularly, we show that the combination of composition and union yields the structure of a finite idempotent seminearring. We also show that the restricted class of proper Krom-Horn programs, which only contain rules with exactly one body atom, yields a finite idempotent semiring. On the semantic side, we show that the van Emden-Kowalski immediate consequence operator of a program can be represented via composition, which allows us to compute the least model semantics of Horn programs without any explicit reference to operators. As a result, we characterize answer sets algebraically, which bridges the conceptual gap between the syntax and semantics of an answer set program in a mathematically satisfactory way, and which provides an algebraic characterization of strong and uniform equivalence. Moreover, it gives rise to an algebraic meta-calculus for answer set programs. In a broader sense, this paper is a further step towards an algebra of rule-based logical theories and in the future we plan to adapt and generalize the methods of this paper to wider classes of formalisms, most importantly to first-order and disjunctive answer set programs and extensions thereof.

We present an explanation system for applications that leverage Answer Set Programming (ASP). Given a program P, an answer set A of P, and an atom a in the program P, our system generates all explanation graphs of a which help explain why a is true (or false) given the program P and the answer set A. We illustrate the functionality of the system using some examples from the literature.

Several forms of iterable belief change exist, differing in the kind of change and its strength: some operators introduce formulae, others remove them; some add formulae unconditionally, others only as additions to the previous beliefs; some only relative to the current situation, others in all possible cases. A sequence of changes may involve several of them: for example, the first step is a revision, the second a contraction and the third a refinement of the previous beliefs. The ten operators considered in this article are shown to be all reducible to three: lexicographic revision, refinement and severe withdrawal. In turn, these three can be expressed in terms of lexicographic revision at the cost of restructuring the sequence. This restructuring needs not to be done explicitly: an algorithm that works on the original sequence is shown. The complexity of mixed sequences of belief change operators is also analyzed. Most of them require only a polynomial number of calls to a satisfiability checker, some are even easier.

The OSSU curriculum is a complete education in computer science using online materials. It's for those who want a proper, well-rounded grounding in concepts fundamental to all computing disciplines, and for those who have the discipline, will, and (most importantly!) good habits to obtain this education largely on their own, but with support from a worldwide community of fellow learners. It is designed according to the degree requirements of undergraduate computer science majors, minus general education (non-CS) requirements, as it is assumed most of the people following this curriculum are already educated outside the field of CS. The courses themselves are among the very best in the world, often coming from Harvard, Princeton, MIT, etc., but specifically chosen to meet the following criteria. When no course meets the above criteria, the coursework is supplemented with a book.

The quest for acquiring a formal representation of the knowledge of a domain of interest has attracted researchers with various backgrounds into a diverse field called ontology learning. We highlight classical machine learning and data mining approaches that have been proposed for (semi-)automating the creation of description logic (DL) ontologies. These are based on association rule mining, formal concept analysis, inductive logic programming, computational learning theory, and neural networks. We provide an overview of each approach and how it has been adapted for dealing with DL ontologies. Finally, we discuss the benefits and limitations of each of them for learning DL ontologies.

Answer set programming (ASP) is a popular nonmonotonic-logic based paradigm for knowledge representation and solving combinatorial problems. Computing the answer set of an ASP program is NP-hard in general, and researchers have been investing significant effort to speed it up. The majority of current ASP solvers employ SAT solver-like technology to find these answer sets. As a result, justification for why a literal is in the answer set is hard to produce. There are dependency graph based approaches to find answer sets, but due to the representational limitations of dependency graphs, such approaches are limited. We propose a novel dependency graph-based approach for finding answer sets in which conjunction of goals is explicitly represented as a node which allows arbitrary answer set programs to be uniformly represented. Our representation preserves causal relationships allowing for justification for each literal in the answer set to be elegantly found. Performance results from an implementation are also reported. Our work paves the way for computing answer sets without grounding a program.

In 2021, a workshop was convened at the Broad Institute of MIT and Harvard to explore potential applications of formal methods and programming language theory to software platforms being developed in the life sciences. The vision to host this workshop at the Broad Institute originated in conversations about economic incentives, the exponential growth of multi-modal data sources, and challenging biomedical problems that have resulted in the life sciences emerging as both key consumers and producers of software and AI/ML technologies [1-4]. We view this next decade as a critical growth phase for this process and an opportunity to shape the software engineering culture of the life sciences from the ground up. Safety and security, realized through both informal and formal methods, are central to this goal [5-7]. The result of these conversations was the event Formal Methods for the Informal Engineer (FMIE), a workshop aimed at highlighting recent successes in the development of verified software.