This paper is aimed as a contribution to the use of formal modal languages in Artificial Intelligence. We introduce a multi-modal version of Second-order Propositional Modal Logic (SOPML), an extension of modal logic with propositional quantification, and illustrate its usefulness as a specification language for knowledge representation as well as temporal and spatial reasoning. Then, we define novel notions of (bi)simulation and prove that these preserve the interpretation of SOPML formulas. Finally, we apply these results to assess the expressive power of SOPML.

Boolean functions in Answer Set Programming have proven a useful modelling tool. They are usually specified by means of aggregates or external atoms. A crucial step in computing answer sets for logic programs containing Boolean functions is verifying whether partial interpretations satisfy a Boolean function for all possible values of its undefined atoms. In this paper, we develop a new methodology for showing when such checks can be done in deterministic polynomial time. This provides a unifying view on all currently known polynomial-time decidability results, and furthermore identifies promising new classes that go well beyond the state of the art. Our main technique consists of using an ordering on the atoms to significantly reduce the necessary number of model checks. For many standard aggregates, we show how this ordering can be automatically obtained.

The dinner speech at the Fischerhuette was given by Jörg Siekmann (University of Saarbrücken). The poster session, consisting of 18 posters and demos, was jointly organized as a get-together with the Berlin Semantic Web Meetup. At the session, wine, beer, and finger food were provided in the greenhouses of the Computer Science Department at The Thirty-First AAAI Conference on Artificial Intelligence the Freie Universität Berlin. The organizers also used (AAAI-17) and the Twenty-Ninth Conference on Innovative this unique opportunity to hold a joint public Applications of Artificial Intelligence (IAAI-17), will be RuleML and RR business meeting as well as an invited held in New Orleans, Louisiana, USA, during the mid-January dinner with all chairs, and invited keynote speakers to mid-February timeframe. AAAI-17 August 1, a boat sightseeing tour from lake Wannsee will arrive in New Orleans just prior to Mardi Gras and festivities to the Reichstag on Sunday, August 2, the CADE exhibitions will already be underway.

We present JudgeD, a probabilistic datalog. A JudgeD program defines a distribution over a set of traditional datalog programs by attaching logical sentences to clauses to implicitly specify traditional data programs. Through the logical sentences, JudgeD provides a novel method for the expression of complex dependencies between both rules and facts. JudgeD is implemented as a proof-of-concept in the language Python. The implementation allows connection to external data sources, and features both a Monte Carlo probability approximation as well as an exact solver supported by BDDs. Several directions for future work are discussed and the implementation is released under the MIT license.

While there exist several approaches in the constraint programming community to learn a constraint theory, few of them have considered the learning of constraint optimization problems.To alleviate this situation, we introduce an initial approach to learning first-order weighted MAX-SAT theories. It employs inductive logic programming techniques to learn a set of first-order clauses and then uses preference learning techniques to learn the weights of the clauses.In order to learn these weighted clauses, the clausal optimization system uses examples of possible worlds and a set of preferences that state which examples are preferred over other ones.The technique is also empirically evaluated on a number of examples.These experiments show that the system is capable of learning clauses and weights that accurately capture underlying models.

Recent work by Janhunen, Tasharrofi, and Ternovska (2016) started from the following observation: "if SAT From the result of this oracle call, a learned clause is generated and added to ϕ. Now that formalism; (2) It can be immediately combined with other these highly-performant SATsolvers exist, research often SAT extensions (such as integer variables, acyclicity, or any stretches beyond SAT, either because of trying to tackle other theory propagator); (3) No dedicated propagators need problems of a complexity higher than NP or because the input to be developed for the new extension because the nested format of SAT solvers (propositional logic) is too limited solver is (automatically) used as a propagator for its internal to concisely and naturally express certain domain specific theory; for example, it was shown by Janhunen, Tasharrofi, constraints, such as graph properties.

We investigate two QBF resolution systems that use extension variables: weak extended Q-resolution, where the extension variables are quantified at the innermost level, and extended Q-resolution, where the extension variables can be placed inside the quantifier prefix. These systems have been considered previously by Wintersteiger et al, who give experimental evidence that extended Q-resolution is stronger than weak extended Q-resolution. Here we prove an exponential separation between the two systems, thereby confirming the conjecture of Wintersteiger et al. Conceptually, this separation relies on showing strategy extraction for weak extended Q-resolution by bounded-depth circuits. In contrast, we show that this strong strategy extraction result fails in extended Q-resolution.

2QBF is a special case of general quantified Boolean formulae (QBF). It is limited to just two quantification levels, i.e., to a form forall-exists. Despite this limitation it applies to a wide range of applications, e.g., to artificial intelligence, graph theory, synthesis, etc.. Recent research showed that CEGAR-based methods give a performance boost to QBF solving (e.g, compared to QDPLL). Conjunctive normal form (CNF) is a commonly accepted representation for both SAT and QBF problems; however, it does not reflect the circuit structure that might be present in the problem. Existing attempts of extracting this structure from CNF and using it in 2QBF context do not show advantages over CNF based 2QBF solvers. In this work we introduce a new workflow for 2QBF, containing a new semantic circuit extraction algorithm and a CEGAR-based 2QBF solver that uses circuit structure and is improved by a so-called "cofactor sharing'' heuristics. We evaluate the proposed methodology on a range of benchmarks and show the practicality of the new approach.

We present RELOOP, a domain-specific language for relational optimization embedded in Python. It allows the user to express relational optimization problems in a natural syntax that follows logic and linear algebra, rather than in the restrictive standard form required by solvers, and can automatically compile the model to a lower-order but equivalent model. Moreover, RELOOP makes it easy to combine relational optimization with high-level features of Python such as loops, parallelism and interfaces to relational databases.

Over the last decade, building on advances in the areas of knowledge compilation and weighted model counting has drastically increased the scalability of inference in probabilistic logic programs. In this paper, we provide an overview of how this has been possible and point out some open challenges.