In this paper, we take a fresh look at three Popperian concepts: riskiness, falsifiability, and truthlikeness (or verisimilitude) of scientific hypotheses or theories. First, we make explicit the dimensions that underlie the notion of riskiness. Secondly, we examine if and how degrees of falsifiability can be defined, and how they are related to various dimensions of the concept of riskiness as well as the experimental context. Thirdly, we consider the relation of riskiness to (expected degrees of) truthlikeness. Throughout, we pay special attention to probabilistic theories and we offer a tentative, quantitative account of verisimilitude for probabilistic theories. "Modern logic, as I hope is now evident, has the effect of enlarging our abstract imagination, and providing an infinite number of possible hypotheses to be applied in the analysis of any complex fact." A theory is falsifiable if it allows us to deduce predictions that can be compared to evidence, which according ...

Knowledge compilation (KC) languages find a growing number of practical uses, including in Constraint Programming (CP) and in Machine Learning (ML). In most applications, one natural question is how to explain the decisions made by models represented by a KC language. This paper shows that for many of the best known KC languages, well-known classes of explanations can be computed in polynomial time. These classes include deterministic decomposable negation normal form (d-DNNF), and so any KC language that is strictly less succinct than d-DNNF. Furthermore, the paper also investigates the conditions under which polynomial time computation of explanations can be extended to KC languages more succinct than d-DNNF.

Proofs of unsatisfiability of a negated conjecture, or, equivalently, proofs of validity of the original conjecture, are an essential output of automated reasoning methods. The transformation, exchange, and standardization of proofs is a key factor for the interoperability of different automated reasoning systems. In theorem proving proof reconstruction is the task of extracting a proof from the final state of a derivation after generating the empty clause. While for several theorem proving methods and theorem provers it is a standard task, it is never trivial. For example, in parallel theorem proving with distributed search (see [6] for a recent survey), multiple parallel processes perform inferences and search for a proof.

In this article we present the motivation and the core thesis towards the implementation of a Quantum Knowledge Seeking Agent (QKSA). QKSA is a general reinforcement learning agent that can be used to model classical and quantum dynamics. It merges ideas from universal artificial general intelligence, constructor theory and genetic programming to build a robust and general framework for testing the capabilities of the agent in a variety of environments. It takes the artificial life (or, animat) path to artificial general intelligence where a population of intelligent agents are instantiated to explore valid ways of modelling the perceptions. The multiplicity and survivability of the agents are defined by the fitness, with respect to the explainability and predictability, of a resource-bounded computational model of the environment. This general learning approach is then employed to model the physics of an environment based on subjective observer states of the agents. A specific case of quantum process tomography as a general modelling principle is presented. The various background ideas and a baseline formalism are discussed in this article which sets the groundwork for the implementations of the QKSA that are currently in active development.

Stochastic local search (SLS) is a successful paradigm for solving the satisfiability problem of propositional logic. A recent development in this area involves solving not the original instance, but a modified, yet logically equivalent one. Empirically, this technique was found to be promising as it improves the performance of state-of-the-art SLS solvers. Currently, there is only a shallow understanding of how this modification technique affects the runtimes of SLS solvers. Thus, we model this modification process and conduct an empirical analysis of the hardness of logically equivalent formulas. Our results are twofold. First, if the modification process is treated as a random process, a lognormal distribution perfectly characterizes the hardness; implying that the hardness is long-tailed. This means that the modification technique can be further improved by implementing an additional restart mechanism. Thus, as a second contribution, we theoretically prove that all algorithms exhibiting this long-tail property can be further improved by restarts. Consequently, all SAT solvers employing this modification technique can be enhanced.

Reasoning on defeasible knowledge is a topic of interest in the area of description logics, as it is related to the need of representing exceptional instances in knowledge bases. In this direction, in our previous works we presented a framework for representing (contextualized) OWL RL knowledge bases with a notion of justified exceptions on defeasible axioms: reasoning in such framework is realized by a translation into ASP programs. The resulting reasoning process for OWL RL, however, introduces a complex encoding in order to capture reasoning on the negative information needed for reasoning on exceptions. In this paper, we apply the justified exception approach to knowledge bases in $\textit{DL-Lite}_{\cal R}$, i.e., the language underlying OWL QL. We provide a definition for $\textit{DL-Lite}_{\cal R}$ knowledge bases with defeasible axioms and study their semantic and computational properties. In particular, we study the effects of exceptions over unnamed individuals. The limited form of $\textit{DL-Lite}_{\cal R}$ axioms allows us to formulate a simpler ASP encoding, where reasoning on negative information is managed by direct rules. The resulting materialization method gives rise to a complete reasoning procedure for instance checking in $\textit{DL-Lite}_{\cal R}$ with defeasible axioms. Under consideration in Theory and Practice of Logic Programming (TPLP).

Lehmann and Magidor's rational closure is acknowledged as a landmark in the field of non-monotonic logics and it has also been re-formulated in the context of Description Logics (DLs). We show here how to model a rational form of entailment for expressive DLs, such as SROIQ, providing a novel reasoning procedure that compiles a non-monotone DL knowledge base into a description logic program (dl-program).

Automated commonsense reasoning is essential for building human-like AI systems featuring, for example, explainable AI. Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains (e.g., time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query-driven, top-down execution model for Predicate Answer Set Programming with Constraints, to model and reason using EC. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks in domains featuring constraints involving both dense time and dense fluents.

The modern world runs on software. However, there is a catch: computer code often contains programming errors--some small, some large. These glitches can lead to unexpected results--and systematic failures. "In many cases, software flaws don't make any difference. In other cases, they can cause massive problems," says Kathleen Fisher, professor and chair of the computer science department at Tufts University and a former official of the U.S. Defense Advanced Research Projects Agency (DARPA).

In 1969, Tony Hoare published a classical Communications' article, "An Axiomatic Basis for Computer Programming." Hoare's article culminated a sequence of works by Turing, McCarthy, Wirth, Floyd, and Manna, whose essence is an association of a proposition with each point in the program control flow, where the proposition is asserted to hold whenever that point is reach. Hoare added two important elements to that approach. First, he described a formal logic, now called Hoare Logic, for reasoning about programs. Second, he offered a compelling vision for the program-verification project: "When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics."