In this paper a proof system is developed for plan verification problems $\{X\}c\{Y\}$ and $\{X\}c\{KW p\}$ under 0-approximation semantics for ${\mathcal A}_K$. Here, for a plan $c$, two sets $X,Y$ of fluent literals, and a literal $p$, $\{X\}c\{Y\}$ (resp. $\{X\}c\{KW p\}$) means that all literals of $Y$ become true (resp. $p$ becomes known) after executing $c$ in any initial state in which all literals in $X$ are true.Then, soundness and completeness are proved. The proof system allows verifying plans and generating plans as well.

Boolean optimization finds a wide range of application domains, that motivated a number of different organizations of Boolean optimizers since the mid 90s. Some of the most successful approaches are based on iterative calls to an NP oracle, using either linear search, binary search or the identification of unsatisfiable sub-formulas. The increasing use of Boolean optimizers in practical settings raises the question of confidence in computed results. For example, the issue of confidence is paramount in safety critical settings. One way of increasing the confidence of the results computed by Boolean optimizers is to develop techniques for validating the results. Recent work studied the validation of Boolean optimizers based on branch-and-bound search. This paper complements existing work, and develops methods for validating Boolean optimizers that are based on iterative calls to an NP oracle. This entails implementing solutions for validating both satisfiable and unsatisfiable answers from the NP oracle. The work described in this paper can be applied to a wide range of Boolean optimizers, that find application in Pseudo-Boolean Optimization and in Maximum Satisfiability. Preliminary experimental results indicate that the impact of the proposed method in overall performance is negligible.

This is the third of three papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high-performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal has been to define a representation in which this structure is apparent and can be exploited to improve computational performance. The first paper surveyed existing work that (knowingly or not) exploited problem structure to improve the performance of satisfiability engines, and the second paper showed that this structure could be understood in terms of groups of permutations acting on individual clauses in any particular Boolean theory. We conclude the series by discussing the techniques needed to implement our ideas, and by reporting on their performance on a variety of problem instances.

We present a uniform non-monotonic solution to the problems of reasoning about action on the basis of an argumentation-theoretic approach. Our theory is provably correct relative to a sensible minimisation policy introduced on top of a temporal propositional logic. Sophisticated problem domains can be formalised in our framework. As much attention of researchers in the field has been paid to the traditional and basic problems in reasoning about actions such as the frame, the qualification and the ramification problems, approaches to these problems within our formalisation lie at heart of the expositions presented in this paper.

This is the second of three planned papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal is to define a representation in which this structure is apparent and can easily be exploited to improve computational performance. This paper presents the theoretical basis for the ideas underlying ZAP, arguing that existing ideas in this area exploit a single, recurring structure in that multiple database axioms can be obtained by operating on a single axiom using a subgroup of the group of permutations on the literals in the problem. We argue that the group structure precisely captures the general structure at which earlier approaches hinted, and give numerous examples of its use. We go on to extend the Davis-Putnam-Logemann-Loveland inference procedure to this broader setting, and show that earlier computational improvements are either subsumed or left intact by the new method. The third paper in this series discusses ZAPs implementation and presents experimental performance results.

A grounding of a formula $\phi$ over a given finite domain is a ground formula which is equivalent to $\phi$ on that domain. Very effective propositional solvers have made grounding-based methods for problem solving increasingly important, however for realistic problem domains and instances, the size of groundings is often problematic. A key technique in ground (e.g., SAT) solvers is unit propagation, which often significantly reduces ground formula size even before search begins. We define a "lifted" version of unit propagation which may be carried out prior to grounding, and describe integration of the resulting technique into grounding algorithms. We describe an implementation of the method in a bottom-up grounder, and an experimental study of its performance.

When formalizing proofs with interactive theorem provers, it often happens that extra background knowledge (declarative or procedural) about mathematical concepts is employed without the formalizer explicitly invoking it, to help the formalizer focus on the relevant details of the proof. In the contexts of producing and studying a formalized mathematical argument, such mechanisms are clearly valuable. But we may not always wish to suppress background knowledge. For certain purposes, it is important to know, as far as possible, precisely what background knowledge was implicitly employed in a formal proof. In this note we describe an experiment conducted on the MIZAR Mathematical Library of formal mathematical proofs to elicit one such class of implicitly employed background knowledge: properties of functions and relations (e.g., commutativity, asymmetry, etc.).

Publishing private data on external servers incurs the problem of how to avoid unwanted disclosure of confidential data. We study a problem of confidentiality in extended disjunctive logic programs and show how it can be solved by extended abduction. In particular, we analyze how credulous non-monotonic reasoning affects confidentiality.

Statistical relational learning techniques have been successfully applied in a wide range of relational domains. In most of these applications, the human designers capitalized on their background knowledge by following a trial-and-error trajectory, where relational features are manually defined by a human engineer, parameters are learned for those features on the training data, the resulting model is validated, and the cycle repeats as the engineer adjusts the set of features. This paper seeks to streamline application development in large relational domains by introducing a light-weight approach that efficiently evaluates relational features on pieces of the relational graph that are streamed to it one at a time. We evaluate our approach on two social media tasks and demonstrate that it leads to more accurate models that are learned faster.

In this paper we present a proposal for a knowledge-based programming environment. In such an environment, declarative background knowledge, procedures, and concrete data are represented in suitable languages and combined in a flexible manner. This leads to a highly declarative programming style. We illustrate our approach on an example and report about our prototype implementation.