We reformulate Pratt's tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and more direct for implementation. Extending the method we give the first EXPTIME (optimal) tableau decision procedure not based on transformation for checking consistency of an ABox w.r.t. a TBox in PDL (here, PDL is treated as a description logic). We also prove the new result that the data complexity of the instance checking problem in PDL is coNP-complete.

Thanks to recent advances, AI Planning has become the underlying technique for several applications. Figuring prominently among these is automated Web Service Composition (WSC) at the "capability" level, where services are described in terms of preconditions and effects over ontological concepts. A key issue in addressing WSC as planning is that ontologies are not only formal vocabularies; they also axiomatize the possible relationships between concepts. Such axioms correspond to what has been termed "integrity constraints" in the actions and change literature, and applying a web service is essentially a belief update operation. The reasoning required for belief update is known to be harder than reasoning in the ontology itself. The support for belief update is severely limited in current planning tools. Our first contribution consists in identifying an interesting special case of WSC which is both significant and more tractable. The special case, which we term "forward effects", is characterized by the fact that every ramification of a web service application involves at least one new constant generated as output by the web service. We show that, in this setting, the reasoning required for belief update simplifies to standard reasoning in the ontology itself. This relates to, and extends, current notions of "message-based" WSC, where the need for belief update is removed by a strong (often implicit or informal) assumption of "locality" of the individual messages. We clarify the computational properties of the forward effects case, and point out a strong relation to standard notions of planning under uncertainty, suggesting that effective tools for the latter can be successfully adapted to address the former. Furthermore, we identify a significant sub-case, named "strictly forward effects", where an actual compilation into planning under uncertainty exists. This enables us to exploit off-the-shelf planning tools to solve message-based WSC in a general form that involves powerful ontologies, and requires reasoning about partial matches between concepts. We provide empirical evidence that this approach may be quite effective, using Conformant-FF as the underlying planner.

The logic which describes quantum robots is not orthodox quantum logic, but a deductive calculus which reproduces the quantum tasks (computational processes, and actions) taking into account quantum superposition and quantum entanglement. A way toward the realization of intelligent quantum robots is to adopt a quantum metalanguage to control quantum robots. A physical implementation of a quantum metalanguage might be the use of coherent states in brain signals.

In a case study we investigate whether off the shelf higher-order theorem provers and model generators can be employed to automate reasoning in and about quantified multimodal logics. In our experiments we exploit the new TPTP infrastructure for classical higher-order logic.

When mathematicians present proofs they usually adapt their explanations to their didactic goals and to the (assumed) knowledge of their addressees. Modern automated theorem provers, in contrast, present proofs usually at a fixed level of detail (also called granularity). Often these presentations are neither intended nor suitable for human use. A challenge therefore is to develop user- and goal-adaptive proof presentation techniques that obey common mathematical practice. We present a flexible and adaptive approach to proof presentation that exploits machine learning techniques to extract a model of the specific granularity of proof examples and employs this model for the automated generation of further proofs at an adapted level of granularity.

Numerous logic frameworks have been proposed for modeling uncertainty and reasoning with such data. While different in syntax, the approaches of these frameworks have been classified into "annotation based" (AB) and "implication based" (IB). In this paper, we present a unified framework which allows evaluating programs in either approach. It extends existing query processing techniques to handle certainty constraints and uses heuristics to further improve the performance. Our experiments indicate that the proposed techniques yield useful tools for uncertainty reasoning.

The Multiple ANSwer EXtraction system is a framework for interpreting a conjecture with outermost existentially quantified variables as a question, and extracting multiple answers to the question by repetitive calls to a base system that can report the bindings for the variables in one proof of the conjecture. This paper describes the framework and demonstrates its use on an illustrative example.

Coinduction has recently been introduced into logic programming by Simon et al. The resulting paradigm, termed coinductive logic programming (co-LP), allows one to model and reason about infinite processes and objects. Co-LP extended with negation has many interesting applications: for instance in developing top-down, goaldirected evaluation strategies for Answer Set Programming. In this paper we show yet another application of co-LP, namely, elegantly realizing Boolean SAT solvers

Many important tasks can be cast as weighted relational satisfiability problems.  Propositionalizing relational theories and making inferences with them using SAT algorithms has proven effective in many cases.  However, these approaches require that all objects in a domain be known in advance.  Many domains, from language understanding to machine vision, involve reasoning about objects that are not known beforehand.  Theories with unknown objects can require models with infinite objects in their domain and thus lead to propositionalized SAT theories that existing algorithms cannot deal with.  To address these problems, we characterize a class of relational generative weighted satisfiability theories (GenSAT) over potentially infinite domains and propose an algorithm, GenDPLL, for finding models of these theories.  We introduce the notion of a relevant model and an increasing cost theory to identify conditions under which GenDPLL is complete, even when a theory has infinite models.

Graded modal logic is the formal language obtained from ordinary (propositional) modal logic by endowing its modal operators with cardinality constraints. Under the familiar possible-worlds semantics, these augmented modal operators receive interpretations such as "It is true at no fewer than 15 accessible worlds that...", or "It is true at no more than 2 accessible worlds that...". We investigate the complexity of satisfiability for this language over some familiar classes of frames. This problem is more challenging than its ordinary modal logic counterpart--especially in the case of transitive frames, where graded modal logic lacks the tree-model property. We obtain tight complexity bounds for the problem of determining the satisfiability of a given graded modal logic formula over the classes of frames characterized by any combination of reflexivity, seriality, symmetry, transitivity and the Euclidean property.