First-order model counting emerged recently as a novel reasoning task, at the core of efficient algorithms for probabilistic logics. We present a Skolemization algorithm for model counting problems that eliminates existential quantifiers from a first-order logic theory without changing its weighted model count. For certain subsets of first-order logic, lifted model counters were shown to run in time polynomial in the number of objects in the domain of discourse, where propositional model counters require exponential time. However, these guarantees apply only to Skolem normal form theories (i.e., no existential quantifiers) as the presence of existential quantifiers reduces lifted model counters to propositional ones. Since textbook Skolemization is not sound for model counting, these restrictions precluded efficient model counting for directed models, such as probabilistic logic programs, which rely on existential quantification. Our Skolemization procedure extends the applicability of first-order model counters to these representations. Moreover, it simplifies the design of lifted model counting algorithms.

In the past, there have been several attempts to explain logic programming under the well-founded semantics as a logic of inductive definitions. A weakness in all is the absence of an obvious connection between how we understand various types of informal inductive definitions in mathematical text and the complex mathematics of the well-founded semantics. We formalize the induction process in the most common principles and prove that the well-founded model construction generalizes them all.

Extensional higher-order logic programming has been recently proposed as an interesting extension of classical logic programming. An important characteristic of the new paradigm is that it preserves all the well-known properties oftraditional logic programming. In this paper we enhance extensional higher-order logic programming with constructive negation. We argue that the main ideas underlying constructive negation are quite close to the existing proof procedurefor extensional higher-order logic programming and for this reason the two notions amalgamate quite conveniently. We demonstrate the soundness of the resulting proof procedure and describe an actual implementation of a language that embodies the above ideas. In this way we obtain the first (to our knowledge) higher-order logic programming language supporting constructive negation and offering a new style of programming that genuinely extends that of traditional logic programming.

Most logic-based machine learning algorithms rely on an Occamist bias where textual complexity of hypotheses is minimised. Within Inductive Logic Programming (ILP), this approach fails to distinguish between the efficiencies of hypothesised programs, such as quick sort (O(n log n)) and bubble sort (O(n2)).

We consider a simple language for writing causal action theories, and postulate several properties for the state transition models of these theories. We then consider some possible embeddings of these causal action theories in some other action formalisms, and their implementations in logic programs with answer set semantics. In particular, we propose to consider what we call permissible translations from these causal action theories to logic programs. We identify two sets of properties, and prove that for each set, there is only one permissible translation, under strong equivalence, that can satisfy all properties in the set. As it turns out, for one set, the unique permissible translation is essentially the same as Balduccini and Gelfond's translation from Gelfond and Lifschitz's action language B to logic programs. For the other, it is essentially the same as Lifschitz and Turner's translation from the action language C to logic programs. This work provides a new perspective on understanding, evaluating and comparing action languages by using sets of properties instead of examples. It will be interesting to see if other action languages can be similarly characterized, and whether new action formalisms can be defined using different sets of properties.

Preference Inference involves inferring additional user preferences from elicited or observed preferences, based on assumptions regarding the form of the user's preference relation. In this paper we consider a situation in which alternatives have an associated vector of costs, each component corresponding to a different criterion, and are compared using a kind of lexicographic order, similar to the way alternatives are compared in a Hierarchical Constraint Logic Programming model. It is assumed that the user has some (unknown) importance ordering on criteria, and that to compare two alternatives, firstly, the combined cost of each alternative with respect to the most important criteria are compared; only if these combined costs are equal, are the next most important criteria considered. The preference inference problem then consists of determining whether a preference statement can be inferred from a set of input preferences. We show that this problem is co-NP-complete, even if one restricts the cardinality of the equal-importance sets to have at most two elements, and one only considers non-strict preferences. However, it is polynomial if it is assumed that the user's ordering of criteria is a total ordering; it is also polynomial if the sets of equally important criteria are all equivalence classes of a given fixed equivalence relation. We give an efficient polynomial algorithm for these cases, which also throws light on the structure of the inference.

Fundamental to reasoning about actions and beliefs is the projection problem: to decide what is believed after a sequence of actions is performed. Progression is one widely applied technique to solve this problem. In this paper we propose a novel framework for computing progression in the epistemic situation calculus. In particular, we model an agent's preferential belief structure using conditional statements and provide a technique for updating these conditional statements as actions are performed and sensing information is received. Moreover, we show, by using the concepts of natural revision and only-believing, that the progression of a conditional knowledge base can be represented by only-believing the revised set of conditional statements. These results lay the foundations for feasible belief progression due to the unique-model property of only-believing.

Existential rules (also known as Datalog /- or tuple-generating dependencies) have been intensively studied in recent years as a prominent formalism in knowledge representation and database systems. We consider them here as a querying formalism, extending classical Datalog, the language of deductive databases. It is well known that the classes of databases recognized by (Boolean) existential rule queries are closed under homomorphisms. Also, due to the existence of a semi-decision procedure (the chase), these database classes are recursively enumerable. We show that, conversely, every homomorphism-closed recursively enumerable query can be expressed as an existential rule query, thus arriving at a precise characterization of existential rules by model-theoretic and computational properties. Although the result is very intuitive, the proof turns out to be non-trivial. This result can be seen as a very expressive counterpart of the prominent Lyndon-Los-Tarski-Theorem characterizing the homomorphism-closed fragment of first-order logic. Notably, our result does not presume the existence of any additional built-in structure on the queried data, such as a linear order on the domain, which is a typical requirement for other characterizations in the spirit of descriptive complexity.

The sentential decision diagram (SDD) has been recently proposed as a new tractable representation of Boolean functions that generalizes the influential ordered binary decision diagram (OBDD). Empirically, compiling CNFs into SDDs has yielded significant improvements in both time and space over compiling them into OBDDs, using a bottom-up compilation approach. In this work, we present a top-down CNF to SDD compiler that is based on techniques from the SAT literature. We compare the presented compiler empirically to the state-of-the-art, bottom-up SDD compiler, showing orders-of-magnitude improvements in compilation time.

Forgetting is an important mechanism for logic-based agent systems. A recent interest has been in the desirable properties of forgetting in answer set programming (ASP)and their impact on the design of forgetting operators. It is known that some subsets of these propertiesare incompatible, i.e., they cannot be satisfied at the same time. In this paper, we are interested in the question onthe largest set Δ of pairs (Π, V), where Π is a logic program and V is a set of atoms, such that a forgetting operator exists that satisfies all the desirable properties for each (Π, V) in Δ. We answer this question positively by discovering the precise condition under which the knowledge forgetting, a well-established approach to forgetting in ASP, satisfies the property of strong persistence, which leads to a sufficient and necessary condition for a forgetting operator to satisfy all the desirable properties proposed in the literature. We explore computational complexities on checking the condition and present a syntactic characterization which can serve as the basis of computing knowledge forgetting in ASP.