We address the problem of belief change in (nonmonotonic) logic programming under answer set semantics. Unlike previous approaches to belief change in logic programming, our formal techniques are analogous to those of distance-based belief revision in propositional logic. In developing our results, we build upon the model theory of logic programs furnished by SE models. Since SE models provide a formal, monotonic characterisation of logic programs, we can adapt techniques from the area of belief revision to belief change in logic programs. We introduce methods for revising and merging logic programs, respectively. For the former, we study both subset-based revision as well as cardinality-based revision, and we show that they satisfy the majority of the AGM postulates for revision. For merging, we consider operators following arbitration merging and IC merging, respectively. We also present encodings for computing the revision as well as the merging of logic programs within the same logic programming framework, giving rise to a direct implementation of our approach in terms of off-the-shelf answer set solvers. These encodings reflect in turn the fact that our change operators do not increase the complexity of the base formalism.

We propose a database model that allows users to annotate data with belief statements. Our motivation comes from scientific database applications where a community of users is working together to assemble, revise, and curate a shared data repository. As the community accumulates knowledge and the database content evolves over time, it may contain conflicting information and members can disagree on the information it should store. For example, Alice may believe that a tuple should be in the database, whereas Bob disagrees. He may also insert the reason why he thinks Alice believes the tuple should be in the database, and explain what he thinks the correct tuple should be instead. We propose a formal model for Belief Databases that interprets users' annotations as belief statements. These annotations can refer both to the base data and to other annotations. We give a formal semantics based on a fragment of multi-agent epistemic logic and define a query language over belief databases. We then prove a key technical result, stating that every belief database can be encoded as a canonical Kripke structure. We use this structure to describe a relational representation of belief databases, and give an algorithm for translating queries over the belief database into standard relational queries. Finally, we report early experimental results with our prototype implementation on synthetic data.

Boolean Satisfiability (SAT) solvers are now routinely used in the verification of large industrial problems. However, their application in safety-critical domains such as the railways, avionics, and automotive industries requires some form of assurance for the results, as the solvers can (and sometimes do) have bugs. Unfortunately, the complexity of modern, highly optimized SAT solvers renders impractical the development of direct formal proofs of their correctness. This paper presents an alternative approach where an untrusted, industrial-strength, SAT solver is plugged into a trusted, formally certified, SAT proof checker to provide industrial-strength certified SAT solving. The key novelties and characteristics of our approach are (i) that the checker is automatically extracted from the formal development, (ii), that the combined system can be used as a standalone executable program independent of any supporting theorem prover, and (iii) that the checker certifies any SAT solver respecting the agreed format for satisfiability and unsatisfiability claims. The core of the system is a certified checker for unsatisfiability claims that is formally designed and verified in Coq. We present its formal design and outline the correctness proofs. The actual standalone checker is automatically extracted from the the Coq development. An evaluation of the certified checker on a representative set of industrial benchmarks from the SAT Race Competition shows that, albeit it is slower than uncertified SAT checkers, it is significantly faster than certified checkers implemented on top of an interactive theorem prover.

Action description languages, such as A and B, are expressive instruments introduced for formalizing planning domains and planning problem instances. The paper starts by proposing a methodology to encode an action language (with conditional effects and static causal laws), a slight variation of B, using Constraint Logic Programming over Finite Domains. The approach is then generalized to raise the use of constraints to the level of the action language itself. A prototype implementation has been developed, and the preliminary results are presented and discussed. To appear in Theory and Practice of Logic Programming (TPLP)

In the recent years rule-based programming in terms of decla rative logic programming has formed the basis for many Artificial In telligence (AI) applications and is well integrated in the mainstream infor mation technology capturing higher-level decision logics. Typically, the st andard rule systems and rule-based logic programming languages such as Prolog deri vatives are based on the untyped theory of predicate calculus with untyped logic al objects (untyped terms), i.e. the logical reasoning algorithms apply pure sy ntactical reasoning. From a rule engineering perspective this is a serious restri ction which lacks major Software Engineering principles such as data abstracti on or modularization, which become more and more important when rule applications grow larger and more complex. To support such principles in logic programmi ng and capture the rule engineer's intended meaning of a logic program, types a nd typed objects play an important role. Moreover, from a computational poin t of view, the use of types drastically reduces the search space, i.e. proofs c an be kept at a more abstract level and it offers the option to restrict the applic ation of rules and to control the level of generality in queries.

We present the first class of mathematically rigorous, general, fully self-referential, self-improving, optimally efficient problem solvers. Inspired by Kurt Goedel's celebrated self-referential formulas (1931), such a problem solver rewrites any part of its own code as soon as it has found a proof that the rewrite is useful, where the problem-dependent utility function and the hardware and the entire initial code are described by axioms encoded in an initial proof searcher which is also part of the initial code. The searcher systematically and efficiently tests computable proof techniques (programs whose outputs are proofs) until it finds a provably useful, computable self-rewrite. We show that such a self-rewrite is globally optimal - no local maxima! - since the code first had to prove that it is not useful to continue the proof search for alternative self-rewrites. Unlike previous non-self-referential methods based on hardwired proof searchers, ours not only boasts an optimal order of complexity but can optimally reduce any slowdowns hidden by the O()-notation, provided the utility of such speed-ups is provable at all.

The axiom scheme of Extensionality states that whenever two predicates or relations are coextensive they must have the same propertie s: XY ( null x(Xnull x Ynull x) Z (ZX ZY)) (1) Historically Extensionality has always been problematic, the main problem being that in many areas of application, though not perhaps in t he foundations of mathematics, the statement is simply false. This was reco gnized by Whitehead and Russell in Principia Mathematica [32], where intensional functions such as ' A believes that p ' or'it is a strange coincidence that p ' are discussed at length. However, in the introduction to the second edition ( 1927) of the Prin-cipia Whitehead and Russell (influenced by Wittgenstein's Tractatus) already entertain the possibility that "all functions of functions are extensional". Thirteen years later, in Church's [6] canonical formulation of t he Theory of Types, it is observed that axioms of Extensionality should be adopt ed "[i]n order to obtain classical real number theory (analysis)", a wording that does not seem to rule out the option of not adopting them. Church's formula tion of type theory was completely syntactic and axioms could be adopted or d ropped at will, The Journal of Symbolic Logic, to appear.

Outsourcing of complex IT infrastructure to IT service providers has increased substantially during the past years. IT service providers must be able to fulfil their service-quality commitments based upon predefined Service Level Agreements (SLAs) with the service customer. They need to manage, execute and maintain thousands of SLAs for different customers and different types of services, which needs new levels of flexibility and automation not available with the current technology. The complexity of contractual logic in SLAs requires new forms of knowledge representation to automatically draw inferences and execute contractual agreements. A logic-based approach provides several advantages including automated rule chaining allowing for compact knowledge representation as well as flexibility to adapt to rapidly changing business requirements. We suggest adequate logical formalisms for representation and enforcement of SLA rules and describe a proof-of-concept implementation. The article describes selected formalisms of the ContractLog KR and their adequacy for automated SLA management and presents results of experiments to demonstrate flexibility and scalability of the approach.

We present tableau calculi for some logics of nonmonotonic reasoning, as defined by Kraus, Lehmann and Magidor. We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative and rational logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. We provide a decision procedure for the logics considered, and we study their complexity.

INRA Toulouse, France Abstract Weighted Max-SA T is the optimization version of SA T and many important problems can be naturally encoded as such. Solving weighted Max-SA T is an important problem from both a theoretical and a practical point of view. In recent ye ars, there has been considerable interest in finding efficient solving techniques. Most of thi s work focus on the computation of good quality lower bounds to be used within a branch and bou nd DPLL-like algorithm. Most often, these lower bounds are described in a procedural way. Because of that, it is difficult to realize the logic that is behind. In this paper we introduce an original framework for Max-SA T that stresses the parallelism with classical SA T. Then, we extend the two basic SA T s olving techniques: search and inference. We show that many algorithmic tricks used in state-of-the-art Max-SA T solvers are easily expressable in logic terms with our framework in a unified manner. Besides, we introduce an original search algorithm that per forms a restricted amount of weighted resolution at each visited node. We empirically compare our algorithm w ith a variety of solving alternatives on several benchmarks. Our experiments, which constitute to the best of our knowledge the most comprehensive Max-sat eva luation ever reported, show that our algorithm is generally orders of magnitude faster t han any competitor. Preprint submitted to Elsevier Science 11 September 2018 1 Introduction Weighted Max-SA T is the optimization version of the SA T prob lem and many important problems can be naturally expressed as such. In recent years, there has been a considerable effort in finding efficient exact algorithms. A common drawback of all these alg orithms is that albeit the close relationship between SA T and Max-SA T, they cannot be easily described with logic terminology. For instance, the contributions of [11,12,13,14] are good quality lower bounds to be incorporated into a depth-first branch and bound procedure. These lower bounds are mostly defined in a procedural way and it is very difficult to see the logic that is behind the execution of the procedure. This is in contrast with SA T algorithms where the solving process can b e easily decomposed into atomic logical steps. In this paper we introduce an original framework for (weight ed) Max-SA T in which the notions of upper and lower bound are incorporated into the problem definition. Under this framework classical SA T is just a particular case of Max-SA T, and the main SA T solving techniques can be naturally extended. In pa rticular, we extend the basic simplification rules (for example, idempotency, absorption, unit clause reduction, etc) and introduce a new one, hardening, that does not make sense in the SA T context.