Classic entrenchment-based contraction is not applicable to many useful logics, such as description logics. This is because the semantic construction refers to arbitrary disjunctions of formulas, while many logics do not fully support disjunction. In this paper, we present a new entrenchment-based contraction which does not rely on any logical connectives except conjunction. This contraction is applicable to all fragments of first-order logic that support conjunction. We provide a representation theorem for the contraction which shows that it satisfies all the AGM postulates except for the controversial Recovery Postulate, and is a natural generalisation of entrenchment-based contraction.

A consequence of a logic program is a consistent set of literals that are satisfied by every answer set. The well-founded model is a consequence that can be used to simplify the logic program. In this paper, we extend the notion of well-founded models to consequences for simplifying disjunctive logic programs (DLPs) in a general manner. Specifically, we provide two main notions, strong reliable set and weak reliable set, and show that a DLP is strongly equivalent to the simplified program if and only if the consequence is a strong reliable set, and they have the same answer sets if and only if the consequence is a weak reliable set. Then we provide computational complexity on identifying both notions. In addition, we provide an algorithm to compute some strong reliable sets and show that the approach is an extension of the well-founded model in simplifying logic programs.

In this paper, we study the expressive power of first-order disjunctive logic programming (DLP) and normal logic programming (NLP) under the stable model semantics. We show that, unlike the propositional case, first-order DLP is strictly more expressive than NLP. This result still holds even if auxiliary predicates are allowed, assuming that NP not equals to coNP. On the other side, we propose a partial translation from first-order DLP to NLP via unfolding and shifting, which suggests a sound yet incomplete approach to implement DLP via NLP solvers. We also identify some NLP definable subclasses, and conjecture to exactly capture NLP definability by unfolding and shifting.

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.

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.

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.

This choice, which is also related to the finitary and infinitary The model-checking problem for Resource Agent semantics of [Bulling and Farwer, 2010], stipulates whether Logic is known to be undecidable. We review existing in every model, agents always have a choice of doing nothing (un)decidability results and identify a significant (executing an idle action) that produces and consumes fragment of the logic for which model checking no resources [Alechina et al., 2014]. Apart from the technical is decidable. We discuss aspects which makes convenience for model-checking (intuitively it implies model checking decidable and prove undecidability that any strategy to satisfy a next or until formula only needs of two open fragments over a class of models in to ensure the relevant subformula becomes true after finitely which agents always have a choice of doing nothing.

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.

Probabilistic systems are an important theme in AI domain. As the specification language, PCTL is the most frequently used logic for reasoning about probabilistic properties. In this paper, we present a natural and succinct probabilistic extension of Mu-calculus, another prominent logic in the concurrency theory. We study the relationship with PCTL. Surprisingly, the expressiveness is highly orthogonal with PCTL. The proposed logic captures some useful properties which cannot be expressed in PCTL. We investigate the model checking and satisfiability problem, and show that the model checking problem is in UP and co-UP, and the satisfiability checking can be decided via reducing into solving parity games. This is in contrast to PCTL as well, whose satisfiability checking is still an open problem.

When Golog programs are used to control agents' behaviour in a high-level manner, their partial correctness naturally becomes an important concern. In this paper we propose a sound but incomplete method for automatic verification of partial correctness of Golog programs.  We introduce the notion of extended regression, which reduces partial correctness of Golog programs to first-order entailment problems.  During the process loop invariants are automatically discovered by heuristic methods.  We propose progression of small models wrt Golog programs, which are used to filter out too strong heuristic candidates.  In this way we combine the methods of static and dynamic analysis from the software engineering community.  Furthermore, our method can also be adapted to verify state constraints.  Experiments show that our method can not only handle sequential and nested loops uniformly in a reasonable among of time, but also be used to discover succinct and comprehensible loop invariants and state constraints.