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.

Complex Event Recognition (CER) systems detect event occurrences in streaming time-stamped input using predefined event patterns. Logic-based approaches are of special interest in CER, since, via Statistical Relational AI, they combine uncertainty-resilient reasoning with time and change, with machine learning, thus alleviating the cost of manual event pattern authoring. We present a system based on Answer Set Programming (ASP), capable of probabilistic reasoning with complex event patterns in the form of weighted rules in the Event Calculus, whose structure and weights are learnt online. We compare our ASP-based implementation with a Markov Logic-based one and with a number of state-of-the-art batch learning algorithms on CER datasets for activity recognition, maritime surveillance and fleet management. Our results demonstrate the superiority of our novel approach, both in terms of efficiency and predictive performance. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP).

When we say the code on the description tape of the physical UTM "is" We re-evaluate universal computation based on w what we actually mean is, adopting the thermodynamic the synthesis of Turing machines. This leads to a language, that the system is in a phase (a local minima of view of programs as singularities of analytic varieties the free energy) including the microstate c we associate to or, equivalently, as phases of the Bayesian w. However, when the system is in this phase its microstate posterior of a synthesis problem. This new point is not equal to c but rather undergoes rapid spontaneous of view reveals unexplored directions of research transitions between many microstates "near" c. in program synthesis, of which neural networks are a subset, for example in relation to phase transitions, So in any possible physical realisation of a UTM, a program complexity and generalisation. We also is realised by a phase of the physical system. Does this have lay the empirical foundations for these new directions any computational significance?

It is known due to the work of Van den Broeck, Meert and Darwiche that weighted first-order model counting (WFOMC) in the two-variable fragment of first-order logic can be solved in time polynomial in the number of domain elements. In this paper we extend this result to the two-variable fragment with counting quantifiers.

We present a formal language for specifying qualitative preferences over temporal goals and a preference-based planning method in stochastic systems. Using automata-theoretic modeling, the proposed specification allows us to express preferences over different sets of outcomes, where each outcome describes a set of temporal sequences of subgoals. We define the value of preference satisfaction given a stochastic process over possible outcomes and develop an algorithm for time-constrained probabilistic planning in labeled Markov decision processes where an agent aims to maximally satisfy its preference formula within a pre-defined finite time duration. We present experimental results using a stochastic gridworld example and discuss possible extensions of the proposed preference model.