Propositional Typicality Logic (PTL) is a recently proposed logic, obtained by enriching classical propositional logic with a typicality operator. In spite of the non-monotonic features introduced by the semantics adopted for the typicality operator, the obvious Tarskian definition of entailment for PTL remains monotonic and is therefore not appropriate. We investigate different (semantic) versions of entailment for PTL, based on the notion of Rational Closure as defined by Lehmann and Magidor for KLM-style conditionals, and constructed using minimality. Our first important result is an impossibility theorem showing that a set of proposed postulates that at first all seem appropriate for a notion of entailment with regard to typicality cannot be satis- fied simultaneously. Closer inspection reveals that this result is best interpreted as an argument for advocating the development of more than one type of PTL entailment. In the spirit of this interpretation, we define two primary forms of entailment for PTL and discuss their advantages and disadvantages

Approximation fixpoint theory (AFT) is an algebraical study of fixpoints of lattice operators. Recently, AFT was extended with the notion of a grounded fixpoint. This type of fixpoint formalises common intuitions from various application domains of AFT, including logic programming, default logic, autoepistemic logic and abstract argumentation frameworks. The study of groundedness was limited to exact lattice points; in this paper, we extend it to the bilattice: for an approximator A of O, we define A-groundedness.  We show that all partial A-stable fixpoints are A-grounded and that the A-well-founded fixpoint is uniquely characterised as the least precise A-grounded fixpoint.  We apply our theory to logic programming and study complexity.

Interval-based possibilistic logic is a flexible setting extending standard possibilistic logic such that each logical expression is associated with a sub-interval of [0,1]. This paper focuses on the fundamental issue of conditioning in the interval-based possibilistic setting. The first part of the paper first proposes a set of natural properties that an interval-based conditioning operator should satisfy. We then give a natural and safe definition for conditioning an interval-based possibility distribution. This definition is based on applying standard min-based or product-based conditioning on the set of all associated compatible possibility distributions. We analyze the obtained posterior distributions and provide a precise characterization of lower and upper endpoints of the intervals associated with interpretations. The second part of the paper provides an equivalent syntactic computation of interval-based conditioning when interval-based distributions are compactly encoded by means of interval-based possibilistic knowledge bases. We show that interval-based conditioning is achieved without extra computational cost comparing to conditioning standard possibilistic knowledge bases.

High-level programming languages are an influential control paradigm for building agents that are purposeful in an incompletely known world. GOLOG, for example, allows us to write programs, with loops, whose constructs refer to an explicit world model axiomatized in the expressive language of the situation calculus. Over the years, GOLOG has been extended to deal with many other features, the claim being that these would be useful in robotic applications. Unfortunately, when robots are actually deployed, effectors and sensors are noisy, typically characterized over continuous probability distributions, none of which is supported in GOLOG, its dialects or its cousins. This paper presents ALLEGRO, a belief-based programming language for stochastic domains, that refashions GOLOG to allow for discrete and continuous initial uncertainty and noise. It is fully implemented and experiments demonstrate that ALLEGRO could be the basis for bridging high-level programming and probabilistic robotics technologies in a general way.

We introduce epistemic quantified boolean logic (EQBL), an extension of propositional epistemic logic with quantification over propositions. We show that EQBL can express relevant properties about agents’ knowledge in multi-agent contexts, such as “agent a knows as much as agent b”. We analyse the expressiveness of EQBL through a translation into monadic second-order logic, and provide completeness results w.r.t. various classes of Kripke frames. Finally, we prove that model checking EQBL is PSPACE-complete. Thus, the complexity of model checking EQBL is no harder than for (non-modal) quantified boolean logic.

This paper relates two extensively studied formalisms: abstract dialectical frameworks and logic programs with generalized atoms or similar constructs. While the syntactic similarity is easy to see, also a strong relation between various stable model semantics proposed for these formalisms is shown by means of a unifying framework in which these semantics are restated in terms of program reducts and an immediate consequence operator, where program reducts have only minimal differences. This approach has advantages for both formalisms, as for example implemented systems for one formalism are usable for the other, and properties such as computational complexity do not have to be rediscovered. As a first, concrete result of this kind, one stable model semantics based on program reducts and subset-minimality that reached a reasonable consensus for logic programs with generalized atoms provides a novel, alternative semantics for abstract dialectical frameworks.

We present a computational framework for chord invention based on a cognitive-theoretic perspective on conceptual blending. The framework builds on algebraic specifications, and solves two musicological problems. It automatically finds transitions between chord progressions of different keys or idioms, and it substitutes chords in a chord progression by other chords of a similar function, as a means to create novel variations. The approach is demonstrated with several examples where jazz cadences are invented by blending chords in cadences from earlier idioms, and where novel chord progressions are generated by inventing transition chords.

Formula compilation by generation of prime implicates or implicants finds a wide range of applications in AI. Recent work on formula compilation by prime implicate/implicant generation often assumes a Conjunctive/Disjunctive Normal Form (CNF/DNF) representation. However, in many settings propositional formulae are naturally expressed in non-clausal form. Despite a large body of work on compilation of non-clausal formulae, in practice existing approaches can only be applied to fairly small formulae, containing at most a few hundred variables. This paper describes two novel approaches for the compilation of non-clausal formulae either with prime implicants or implicates, that is based on propositional Satisfiability (SAT) solving. These novel algorithms also find application when computing all prime implicates of a CNF formula. The proposed approach is shown to allow the compilation of non-clausal formulae of size significantly larger than existing approaches.

We describe an exact inference-based algorithm for the MinSAT problem. Given a multiset of clauses φ, the algorithm derives as many empty clauses as the maximum number of clauses that can be falsified in φ by applying finitely many times an inference rule, and returns an optimal assignment. We prove the correctness of the algorithm, describe how it can be extended to deal with weighted MinSAT and weighted partial MinSAT instances, analyze the differences between the MaxSAT and MinSAT inference schemes, and define and empirically evaluate the MinSAT Pure Literal Rule.

Existing techniques for inference in probabilistic logic programs are sequential: they first compute the relevant propositional formula for the query of interest, then compile it into a tractable target representation and finally, perform weighted model counting on the resulting representation. We propose Tp-compilation, a new inference technique based on forward reasoning. Tp-compilation proceeds incrementally in that it interleaves the knowledge compilation step for weighted model counting with forward reasoning on the logic program. This leads to a novel anytime algorithm that provides hard bounds on the inferred probabilities. Furthermore, an empirical evaluation shows that Tp-compilation effectively handles larger instances of complex real-world problems than current sequential approaches, both for exact and for anytime approximate inference.