There has been a longstanding dispute over which formalism is the best for representing knowledge in AI. The well-known “declarative vs. procedural controversy” is concerned with the choice of utilizing declarations or procedures as the primary mode of knowledge representation. The ongoing debate between symbolic AI and connectionist AI also revolves around the question of whether knowledge should be represented implicitly (e.g., as parametric knowledge in deep learning and large language models) or explicitly (e.g., as logical theories in traditional knowledge representation and reasoning). To address these issues, we propose a general framework to capture various knowledge representation formalisms in which we are interested. Within the framework, we find a family of universal knowledge representation formalisms, and prove that all universal formalisms are recursively isomorphic. Moreover, we show that all pairwise intertranslatable formalisms that admit the padding property are also recursively isomorphic. These imply that, up to an offline compilation, all universal (or natural and equally expressive) representation formalisms are in fact the same, which thus provides a partial answer to the aforementioned dispute.

General Game Playing (GGP), a research field aimed at developing agents that master different games in a unified way, is regarded as a necessary step towards creating artificial general intelligence. With the success of deep reinforcement learning (DRL) in games like Go, chess, and shogi, it has been recently introduced to GGP and is regarded as a promising technique to achieve the goal of GGP. However, the current work uses fully connected neural networks and is thus unable to efficiently exploit the topological structure of game states. In this paper, we propose an approach to applying general-purposed convolutional neural networks to GGP and implement a DRL-based GGP player. Experiments indicate that the built player not only outperforms the previous algorithm and UCT benchmark in a variety of games but also requires less training time.

Abstract Bisimulations are a key notion to study the expressive power of a modal language. This paper studies the expressivity of Game Description Language (GDL) and its epistemic extension Epistemic GDL (EGDL) through a bisimulation approach. We first define a notion of bisimulation for GDL and prove that it coincides with the indistinguishability of GDL formulas. Based on it, we establish a characterization of the definability of GDL in terms of $k$-bisimulations. Then we design novel notions of bisimulation for EGDL and obtain characterizations of the expressive power of EGDL in terms of them. These characterizations provide a powerful tool to identify the expressive power of game description languages. Finally, we demonstrate with real games that bisimulation can be generalized to capture a wide range of game equivalence.

Existential rule languages are a family of ontology languages that have been widely used in ontology-mediated query answering (OMQA). However, for most of them, the expressive power of representing domain knowledge for OMQA, known as the program expressive power, is not well-understood yet. In this paper, we establish a number of novel characterizations for the program expressive power of several important existential rule languages, including tuple-generating dependencies (TGDs), linear TGDs, as well as disjunctive TGDs. The characterizations employ natural model-theoretic properties, and automata-theoretic properties sometimes, which thus provide powerful tools for identifying the definability of domain knowledge for OMQA in these languages.

Abstract The chase procedure for existential rules is an indispensable tool for several database applications, where its termination guarantees the decidability of these tasks. Most previous studies have focused on the skolem chase variant and its termination analysis. It is known that the restricted chase variant is a more powerful tool in termination analysis provided a database is given. But all-instance termination presents a challenge since the critical database and similar techniques do not work. In this paper, we develop a novel technique to characterize the activeness of all possible cycles of a certain length for the restricted chase, which leads to the formulation of a framework of parameterized classes of the finite restricted chase, called $k$-$\mathsf{safe}(\Phi)$ rule sets. This approach applies to any class of finite skolem chase identified with a condition of acyclicity. More generally, we show that the approach can be applied to the hierarchy of bounded rule sets previously only defined for the skolem chase. Experiments on a collection of ontologies from the web show the applicability of the proposed methods on real-world ontologies.

In this paper, we study an information exchange process in which a network of individuals exchanges a binary opinion.In the process, the individuals change their opinions only if a majority of their neighbours have the opposite opinion and they do it synchronously.Motivated by applications in multiagent systems, distributed computing, and social science, our goal is to derive graphtheoretic features of the network that guarantee whenever a majority of individuals initially have the same opinion, they will eventually spread the opinion to all individuals.We tackle the problem by first introducing a graph-theoretic notion called controlling set which is capable of characterising the information exchange process and, by exploiting the notion, we obtain a series of lower and upper bounds on the in-degree of vertices as well as lower bound on the size of certain neighbourhoods for guaranteeing the majority to unanimity behaviour.

Existential rules, a.k.a. dependencies in databases, and Datalog+/- in knowledge representation and reasoning recently, are a family of important logical languages widely used in computer science and artificial intelligence. Towards a deep understanding of these languages in model theory, we establish model-theoretic characterizations for a number of existential rule languages such as (disjunctive) embedded dependencies, tuple-generating dependencies (TGDs), (frontier-)guarded TGDs and linear TGDs. All these characterizations hold for the class of arbitrary structures, and most of them also work on the class of finite structures. As a natural application of these results, complexity bounds for the rewritability of above languages are also identified.

A logic program with function symbols is called finitely ground if there is a finite propositional logic program whose stable models are exactly the same as the stable models of this program. Finite groundability is an important property for logic programs with function symbols because it makes feasible to compute such programs' stable models using traditional ASP solvers. In this paper, we introduce new decidable classes of finitely ground programs called poly-bounded and k-EXP-bounded programs, which, to the best of our knowledge, strictly contain all other decidable classes of finitely ground programs discovered so far in the literature. We also study the relevant complexity properties for these classes of programs. We prove that the membership complexities for poly-bounded and k-EXP-bounded programs are EXPTIME-complete and (k+1)-EXPTIME-complete, respectively.

Stable model semantics had been recently generalized to non-Herbrand structures by several works, which provides a unified framework and solid logical foundations for answer set programming. This article focuses on the expressiveness of normal and disjunctive logic programs under general stable model semantics. A translation from disjunctive logic programs to normal logic programs is proposed for infinite structures. Over finite structures, some disjunctive logic programs are proved to be intranslatable to normal logic programs if the arities of auxiliary predicates and functions are bounded in a certain way. The equivalence of the expressiveness of normal logic programs and disjunctive logic programs over arbitrary structures is also shown to coincide with that over finite structures and coincide with whether the complexity class NP is closed under complement. Moreover, to obtain a more explicit picture of the expressiveness, some intertranslatability results between logic program classes, and fragments of second-order logic are established.

Classical inconsistency-tolerant query answering relies on selecting maximal components of an ABox/database which are consistent with the ontology. However, some rules in ontologies might be unreliable if they are extracted from ontology learning or written by unskillful knowledge engineers. In this paper we present a framework of handling inconsistent existential rules under stable model semantics, which is defined by a notion called rule repairs to select maximal components of the existential rules. Surprisingly, for R-acyclic existential rules with R-stratified or guarded existential rules with stratified negations, both the data complexity and combined complexity of query answering under the rule repair semantics remain the same as that under the conventional query answering semantics. This leads us to propose several approaches to handle the rule repair semantics by calling answer set programming solvers. An experimental evaluation shows that these approaches have good scalability of query answering under rule repairs on realistic cases.

Sorting is a basic computational task in Computer Science. As a variant of the sorting problem, top-k selecting have been widely used. To our knowledge, on average, the state-of-the-art top-k selecting algorithm Partial Quicksort takes C(n, k) = 2(n+1)Hn+2n-6k+6-2(n+3-k)Hn+1-k comparisons and about C(n, k)/6 exchanges to select the largest k terms from n terms, where Hn denotes the n-th harmonic number. In this paper, a novel top-k algorithm called DC-Top-k is proposed by employing a divide-and-conquer strategy. By a theoretical analysis, the algorithm is proved to be competitive with the state-of-the-art top-k algorithm on the compare time, with a significant improvement on the exchange time. On average, DC-Top-k takes at most (2-1/k)n+O(klog2k) comparisons and O(klog2k) exchanges to select the largest k terms from n terms. The effectiveness of the proposed algorithm is verified by a number of experiments which show that DC-Top-k is 1-3 times faster than Partial Quicksort and, moreover, is notably stabler than the latter. With an increase of k, it is also significantly more efficient than Min-heap based top-k algorithm (U. S. Patent, 2012). In the end, DC-Top-k is naturally implemented in a parallel computing environment, and a better scalability than Partial Quicksort is also demonstrated by experiments.

Finite chase, or alternatively chase termination, is an important condition to ensure the decidability of existential rule languages. In the past few years, a number of rule languages with finite chase have been studied. In this work, we propose a novel approach for classifying the rule languages with finite chase. Using this approach, a family of decidable rule languages, which extend the existing languages with the finite chase property, are naturally defined. We then study the complexity of these languages. Although all of them are tractable for data complexity, we show that their combined complexity can be arbitrarily high. Furthermore, we prove that all the rule languages with finite chase that extend the weakly acyclic language are of the same expressiveness as the weakly acyclic one, while rule languages with higher combined complexity are in general more succinct than those with lower combined complexity.

This paper focuses on computing general first-order parallel and prioritized circumscription with varying constants. We propose linear translations from general first-order circumscription to first-order theories under stable model semantics over arbitrary structures, including Tr_v for parallel circumscription and Tr^s_v for conjunction of parallel circumscriptions (further for prioritized circumscription). To improve the efficiency, we give an optimization \Gamma_{\exists} to reduce logic programs in size when eliminating existential quantifiers during the translations. Based on these results, a general first-order circumscription solver, named cfo2lp, is developed by calling answer set programming (ASP) solvers. Using circuit diagnosis problem and extended stable marriage problem as benchmarks, we compare cfo2lp with a propositional circumscription solver circ2dlp and an ASP solver with complex optimization metasp on efficiency. Experimental results demonstrate that for problems represented by first-order circumscription naturally and intuitively, cfo2lp can compute all solutions over finite structures. We also apply our approach to description logics with circumscription and repairs in inconsistent databases, which can be handled effectively.

Abstract We consider disjunctive logic programs without function symbols but with existential quantification in rule heads, under the semantics of general stable models. There are at least two interesting prospects in these programs. The first is that a program can be made more succinct by using existential variables, and the second is on the potential in representing defeasible ontological knowledge by these logic programs. This paper studies some of the properties of these programs. First, we show a simple yet intuitive definition of stable models for these programs that does not resort to second-order logic. Second, the stable models of these programs can be characterized by an extension of progression for disjunctive programs, which provides a native characterization of justification for stable models. We then study the decidability issue. While the stable model existence problem for safe disjunctive programs is decidable, with existential quantification allowed in rule heads the problem becomes undecidable. We identify an interesting decidable fragment by exploring a new notion of stratification over existential quantification.

The stable model semantics was recently generalized by Ferraris, Lee and Lifschitz to the full first-order language with a syntax translation approach that is very similar to McCarthy's circumscription. In this paper, we investigate the decidability and undecidability of various fragments of first-order language under both semantics of stable models and circumscription. Some maximally decidable classes and undecidable classes are identified. The results obtained in the paper show that the boundaries between decidability and undecidability for these two semantics are very different in spite of the similarity of definition. Moreover, for all fragments considered in the paper, decidability under the semantics of circumscription coincides with that in classical first-order logic. This seems rather counterintuitive due to the second-order definition of circumscription and the high undecidability of first-order circumscription.