By embracing diversity, humanity finds greater strength. Our differences mean we can specialize, using our unique talents to excel in the areas to which we are most suited. This is as true for intelligence as for physical attributes. One person may solve complex algebraic equations for fun but care less about which political party is in power; another may have trouble calculating the tip on a restaurant check but can spend hours discussing the ins and outs of global foreign policy. Both are important skills, but with different applications.

Epistemic Logic Programs (ELPs) are an extension of Answer Set Programming (ASP) with epistemic operators that allow for a form of meta-reasoning, that is, reasoning over multiple possible worlds. Existing ELP solving approaches generally rely on making multiple calls to an ASP solver in order to evaluate the ELP. However, in this paper, we show that there also exists a direct translation from ELPs into non-ground ASP with bounded arity. The resulting ASP program can thus be solved in a single shot. We then implement this encoding method, using recently proposed techniques to handle large, non-ground ASP rules, into the prototype ELP solving system "selp", which we present in this paper. This solver exhibits competitive performance on a set of ELP benchmark instances. Under consideration in Theory and Practice of Logic Programming (TPLP).

Modern applications of artificial intelligence in decision support systems, plan generation systems require reasoning with imprecise a nd uncertain information. Logical frameworks based on bivalent reasoning are not suitable for such applications, because the set {0, 1} cannot capture the vagueness or uncertainty of underlying proposition. Though fuzzy log ic-based systems can represent imprecise linguistic information by ascribi ng membership values to attributes (or truth values to propositions) taken fr om the interval 1 [0,1], but this graded valuation becomes inadequate if the p recise membership can not be determined due to some underlying uncerta inty. This uncertainty may arise from lack of complete information or f rom lack of reliability of source of information or lack of unanimity amon g rational agents in a multi-agent reasoning system or from many other reasons . This uncertainty with respect to the assignment of membership degr ees is captured by assigning a range of possible membership values, i.e. by a ssigning an interval.

In this paper we investigate CNF formulas, for which the unit propagation is strong enough to derive a contradiction if the formula together with a partial assignment of the variables is unsatisfiable (unit refutation complete or URC formulas) or additionally to derive all implied literals if the formula is satisfiable (propagation complete or PC formulas). If a formula represents a function using existentially quantified auxiliary variables, it is called an encoding of the function. We prove several results on the sizes of PC and URC formulas and encodings. One of them are separations between the sizes of formulas of different types. Namely, we prove an exponential separation between the size of URC formulas and PC formulas and between the size of PC encodings using auxiliary variables and URC formulas. Besides of this, we prove that the sizes of any two irredundant PC formulas for the same function differ at most by a polynomial factor in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.

In the 1930s and 40s, around the birth of the "automatic computer", mathematicians wanted to formalise what we mean when we say some result or some function is "effectively computable", whether by machine or human. A "computer", originally, was a person who performed arithmetic calculations. The "effectively" part is included to indicate that we are not concerned with the time any particular computer might take to produce the result, so long as it would get there eventually. They wanted to find the simplest possible system that could be said to compute. Several such systems were invented and for the most part looked entirely unlike each other. Remarkably, they were all eventually shown to be equivalent in the sense that any one could be made to behave like the others.

Synthesizing a program that realizes a logical specification is a classical problem in computer science. We examine a particular type of program synthesis, where the objective is to synthesize a strategy that reacts to a potentially adversarial environment while ensuring that all executions satisfy a Linear Temporal Logic (LTL) specification. Unfortunately, exact methods to solve so-called LTL synthesis via logical inference do not scale. In this work, we cast LTL synthesis as an optimization problem. We employ a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize LTL synthesis. In our experiments the learned Q-function provides effective guidance for synthesis problems with relatively small specifications.

Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019) EPTCS 311, 2019, pp. In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used for other purposes, e.g. for temporal reasoning. Particularly, a quantified modal logic, the deontic cognitive event calculus (DC E C), has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics. Using a fragment of DC E C, we outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation forDC E C . 1 Introduction Modal logics have been used for decades to model and study a diverse set of subjects -- e.g.

I argue that the most interesting goal facing researchers in automated reasoning is being able to solve problems that cannot currently be solved by existing tools and methods. This may appear obvious, and is clearly not an original thought, but focusing on this as a primary goal allows us to examine other goals in a new light. Many successful theorem provers employ a portfolio of different methods for solving problems. This changes the landscape on which we perform our research: solving problems that can already be solved may not improve the state of the art and a method that can solve a handful of problems unsolvable by current methods, but generally performs poorly on most problems, can be very useful. We acknowledge that forcing new methods to compete against portfolio solvers can stifle innovation. However, this is only the case when comparisons are made at the level of total problems solved. We propose a movement towards focussing on unique solutions in evaluation and competitions i.e. measuring the potential contribution to a portfolio solver. This state of affairs is particularly prominent in first-order logic, which is undecidable. When reasoning in a decidable logic there can be a focus on optimising a decision procedure and measuring average solving times. But in a setting where solutions are difficult to find, average solving times lose meaning, and whilst improving the efficiency of a technique can move potential solutions within acceptable time limits, in general, complementary strategies may be more successful.

In recent years, numerous benchmarks for commonsense reasoning have been presented which cover different areas: the Choice of Plausible Alternatives Challenge (COP A) [17] requires causal reasoning in everyday situations, the Winograd Schema Challenge [8] addresses difficult cases of pronoun disambiguation, the TriangleCOP A Challenge [9] focuses on human relationships and emotions, and the Story Cloze Test with the ROCStories Corpora [11] focuses on the ability to determine a plausible ending for a given short story, to name just a few. In our system, we focus on the COP A challenge where each problem consists of a problem description (the premise), a question, and two answer candidates (called alternatives). See Figure 1 for an example. Most approaches tackling these problems are based on machine learning or exploit statistical properties of the natural language input (see e.g.

We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on expanding posets: partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic which we denote $\iltl$, and by imposing additional constraints we obtain the logics $\itlb$ of persistent posets and $\itlht$ of here-and-there temporal logic, both of which have been considered in the literature. We prove that $\iltl$ has the effective finite model property and hence is decidable, while $\itlb$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the `until' and `release' operators are not definable in terms of each other, even over the class of persistent posets.