We study the problem of inducing logic programs in a probabilistic setting, in which both the example descriptions and their classification can be probabilistic. The setting is incorporated in the probabilistic rule learner ProbFOIL+, which combines principles of the rule learner FOIL with ProbLog, a probabilistic Prolog. We illustrate the approach by applying it to the knowledge base of NELL, the Never-Ending Language Learner.

In optimal planning as heuristic search, admissible pruning techniques are paramount. One idea is dominance pruning, identifying states "better than" other states. Prior approaches are limited to simple dominance notions, like "more STRIPS facts true" or "higher resource supply". We apply simulation, well-known in model checking, to compute much more general dominance relations based on comparing transition behavior across states. We do so effectively by expressing state-space simulations through the composition of simulations on orthogonal projections. We show how simulation can be made more powerful by intertwining it with a notion of label dominance. Our experiments show substantial improvements across several IPC benchmark domains.

The use of expressive logical axioms to specify derived predicates often allows planning domains to be formulated more compactly and naturally. We consider axioms in the form of a logic program with recursively defined predicates and negation-as-failure, as in PDDL 2.2. We show that problem formulations with axioms are not only more elegant, but can also be easier to solve, because specifying indirect action effects via axioms removes unnecessary choices from the search space of the planner. Despite their potential, however, axioms are not widely supported, particularly by cost-optimal planners. We draw on the connection between planning axioms and answer set programming to derive a consistency-based relaxation, from which we obtain axiom-aware versions of several admissible planning heuristics, such as hmax and pattern database heuristics.

In this paper, we study synthesis from logical specifications over finite traces expressed in LTLf and its extension LDLf. Specifically, in this form of synthesis, propositions are partitionedin controllable and uncontrollable ones, and the synthesis task consists of setting the controllable propositions over time so that, in spite of how the value of the uncontrollable ones changes, the specification is fulfilled. Conditional planning in presence of declarative and procedural trajectory constraints is a special case of this form of synthesis. We characterize the problem computationally as 2EXPTIME-complete and present a sound and complete synthesis technique based on DFA (reachability) games.

This choice, which is also related to the finitary and infinitary The model-checking problem for Resource Agent semantics of [Bulling and Farwer, 2010], stipulates whether Logic is known to be undecidable. We review existing in every model, agents always have a choice of doing nothing (un)decidability results and identify a significant (executing an idle action) that produces and consumes fragment of the logic for which model checking no resources [Alechina et al., 2014]. Apart from the technical is decidable. We discuss aspects which makes convenience for model-checking (intuitively it implies model checking decidable and prove undecidability that any strategy to satisfy a next or until formula only needs of two open fragments over a class of models in to ensure the relevant subformula becomes true after finitely which agents always have a choice of doing nothing.

Geometry reasoning and proof form a major and challenging component in the K-121 mathematics curriculum. Although several computerized systems exist that help students learn and practice general geometry concepts, they do not target geometry proof problems, which are more advanced and difficult. Powerful geometry theorem provers also exist, however they typically employ advanced algebraic methods and generate complex, difficult to understand proofs, and thus do not meet general K-12 students’ educational needs. This paper tackles these weaknesses of prior systems by introducing a geometry proof system, iGeoTutor, capable of generating human-readable elementary proofs, i.e. proofs using standard Euclidean axioms. We have gathered 77 problems in total from various sources, including ones unsolvable by other systems and from Math competitions. iGeoTutor solves all but two problems in under two minutes each, and more importantly, demonstrates a much more effective and intelligent proof search than prior systems. We have also conducted a pilot study with 12 high school students, and the results show that iGeoTutor provides a clear benefit in helping students learn geometry proofs. We are in active discussions with Khan Academy and local high schools for possible adoption of iGeo-Tutor in real learning environments.

RB+-ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The model-checking problem for RB+-ATL is known to be decidable. However the only available model-checking algorithm for RB+-ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB+-ATL, 1RB+-ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB+-ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces.

Probabilistic systems are an important theme in AI domain. As the specification language, PCTL is the most frequently used logic for reasoning about probabilistic properties. In this paper, we present a natural and succinct probabilistic extension of Mu-calculus, another prominent logic in the concurrency theory. We study the relationship with PCTL. Surprisingly, the expressiveness is highly orthogonal with PCTL. The proposed logic captures some useful properties which cannot be expressed in PCTL. We investigate the model checking and satisfiability problem, and show that the model checking problem is in UP and co-UP, and the satisfiability checking can be decided via reducing into solving parity games. This is in contrast to PCTL as well, whose satisfiability checking is still an open problem.

Compositionality is a fundamental notion in computation whereby complex abstractions can be constructed from simpler ones, but this property has so far escaped the paradigm of end-user programming from examples or natural language. Existing approaches restrict end users to only give holistic end-to-end specifications, which limits the expressivity and scalability of these approaches to relatively simple programs in very restricted domains. In this paper we propose a new approach to end-user program synthesis in which input can be given in a compositional manner through a combination of natural language and examples. We present a domain-agnostic program synthesis algorithm and demonstrate its application to an expressive string manipulation language. We evaluate on a range of complex examples from help forums that are beyond the scope of previous systems.

Word problems are an established technique for teaching mathematical modeling skills in K-12 education. However, many students find word problems unconnected to their lives, artificial, and uninteresting. Most students find them much more difficult than the corresponding symbolic representations. To account for this phenomenon, an ideal pedagogy might involve an individually crafted progression of unique word problems that form a personalized plot. We propose a novel technique for automatic generation of personalized word problems. In our system, word problems are generated from general specifications using answer-set programming (ASP). The specifications include tutor requirements (properties of a mathematical model), and student requirements (personalization, characters, setting). Our system takes a logical encoding of the specification, synthesizes a word problem narrative and its mathematical model as a labeled logical plot graph, and realizes the problem in natural language. Human judges found our problems as solvable as the textbook problems, with a slightly more artificial language.