ABSTRACT. We discuss the role of (variants of) Craig interpolation in description logic research. We start by considering Craig interpolation itself and how it is related to the structure of ontologies and the rewritability of queries in ontology-based data access. We then briefly discuss the role of parallel interpolation (introduced more recently by Parikh et al) for decomposing ontologies. Finally, we consider uniform interpolation - an extension of Craig interpolation in which the interpolant is independent from the formula on the right-hand side. Uniform interpolation has been the focus of significant research activity in Description Logic, with many theoretical results and first implemented systems.

I will not assume any background knowledge about Description Logics but will introduce the relevant notions as required.

ABSTRACT. Ontologies represented using description logics model domains of interest in terms of concepts and binary relations, and are used in a range of areas including medical science, bio-informatics, semantic web or artificial intelligence. Often, ontologies are large and complex and cover 10,000s of concepts. Uniform interpolants are restricted views of ontologies, that only use a specified set of symbols, while preserving all entailments that can be expressed using these symbols. Uniform interpolation can be used for analysing hidden relations in an ontology, removing confidential concepts from an ontology, computing logical differences between ontologies or extracting specialised ontologies for ontology reuse and has many more applications.

We follow a resolution-based approach to make the computation of uniform interpolants of larger ontologies feasable. Uniform interpolants cannot always be represented finitely in the language of the input ontology, for which situation we offer three solutions: extending the signature with additional concepts, approximating the uniform interpolant, or using fixpoint operators.

ABSTRACT. Craig interpolation has been recently shown to be useful in a wide variety of problem domains. One use is in strategy extraction for two player games, as described in our accompanying submission. However, interpolation is not without its drawbacks. It is well-known that an interpolant may be very large and highly redundant. Subsequent use of the interpolant requires that it is transformed to CNF or DNF, which will further increase its size.

We present a new approach to handling both the size of interpolants and transformation to clausal representation. Our approach relies on the observation that in many real-world applications, interpolants are defined over a relatively small set of variables. Additionally, in most cases there likely exists a compact representation of the interpolant in CNF. For instance, in our application to games an interpolant represents a set of winning states that is likely to have a simple structure.

ABSTRACT. We study a general framework for query rewriting in the presence of a domain independent first-order logic theory (a knowledge base) over a signature including database and non-database predicates, based on Craig's interpolant and Beth's definability theorem. In our framework queries are (possibly open) domain independent first-order formulas over the extended signature. The database predicates are meant to be closed, i.e., their extensions are the same in every model since they represent a classical finite relational database, whereas the non-database predicates in the ontology are interpreted classically, i.e., their extensions may vary across different models. It is important to notice that all the conceptual modelling languages devised for the designing of information and database systems (such as Entity-Relationship schemas, UML Class diagrams, Object-Role Modelling ORM diagrams, etc) are domain independent: they can be formalised as domain independent first order theories. Given a domain independent knowledge base and a query implicitly definable from the database signature, the framework provides precise semantic conditions to decide the existence of a domain independent first-order logically equivalent reformulation of the query (called exact rewriting) in terms of the database signature, and if so, it provides an effective approach to construct the reformulation based on interpolation using standard theorem proving techniques (e.g., tableau). We are interested in domain independent reformulations of queries because their range-restricted syntax is needed to reduce the original query answering problem to a relational algebra evaluation over the original database, that is, it is effectively executable as an SQL query directly over the database. Due to the results on the applicability of Beth's theorem and Craig's interpolant, we prove the completeness of our framework in the case of domain independent ontologies and queries expressed in any fragment of first-order logic enjoying finitely controllable determinacy, a stronger property than the finite model property of the logic. If the employed logic does not enjoy finitely controllable determinacy our approach would become sound but incomplete, but still effectively implementable using standard theorem proving techniques. In order to constructively compute the exact domain independent query reformulation we use the tableau based method to find the Craig’s interpolant to compute the from a validity proof of the implication (KB and Q) --> (KB --> Q). Since description logics knowledge bases are not necessarily domain independent, we have syntactically characterised the domain independent fragment of several very expressive fragments of description logics by enforcing a sort of guarded negation, a very reasonable restriction from the point of view of conceptual modelling. These fragments do also enjoy finitely controllable determinacy. We have applied this framework not only to query answering under constraints, but also to data exchange and to view update.

ABSTRACT. Modern Satisfiability Modulo Theories (SMT) solvers are highly efficient and can generate a resolution proof in case of unsatisfiability. Some applications, such as synthesis of Boolean controllers, compute multiple coordinated interpolants from a single refutation proof. In order to do so, the proof is required to have two properties: It must be colorable and local-first. The latter means that resolution over a literal that occurs just in one partition, has to have both premises derived from this partition. Off-the-shelf SMT solvers do not necessarily produce proofs that have these properties. In particular, proofs are usually not local-first. Hofferek et al. 1 suggest to perform proof transformations to obtain a colorable and local-first proof, but these transformations can be computationally expensive. Our goal is to introduce a new method to directly compute a local-first, colorable resolution proof for an unsatisfiable SMT formula. This proof can then be directly used for n-interpolation. Our approach uses a tree-based structure of SMT solvers, where every node in the tree is associated with a formula (possibly empty initially), and a (possibly empty) set of literals. The semantics of the modular SMT problem is the conjunction of the formulas of all nodes. The set of literals associated with a node is computed recursively as follows. Every literal, which appears in more than one descendant of a parent node, is assigned to the parent node. During solving, every node makes decisions about its associated literals only. We start at the root node and communicate the partial assignments to the child nodes until we reach a leaf. Every node has its own solver instance and tries to compute a satisfying assignment w.r.t. the given partial assignments. A blocking clause is added to the parent node if no satisfying assignment can be found. If all child nodes find a satisfying assignment and the conjunction of them is theory-consistent, we either decide more literals, or return to the parent node if we already have a full assignment for all the literals of the current node. In case the conjunction is inconsistent within the theory, we respectively add a blocking clause for the current assignment to the children. In order to obtain this clauses while keeping the modular structure intact, we perform interpolation over the assignments of the children and use the interpolants, which are guaranteed to contain only "global" literals (which can safely be added to the children without breaking the modularity), to learn a blocking clause for every child node. The algorithm terminates if either solely full assignments are communicated to the root node and there is no literal left to decide, or when enough clauses have been learned at the root node to show inconsistency. In the latter case we are able to extract a resolution proof with the same modular structure as the original problem. We are currently working on implementing this approach in the hope that we can use it to generate colorable, local-first proofs for synthesis problems much faster than with post-processing proof transformations.

ABSTRACT. Interpolation has been successfully applied in formal methods for model checking and test-case generation for sequential programs. Security protocols, however, exhibit such idiosyncrasies that make them unsuitable to the direct application of such methods. In this paper, we address this problem and present an interpolation-based method for security protocol verication. Our method starts from a formal protocol specication and combines Craig interpolation, symbolic execution and the standard Dolev-Yao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. We illustrate an implementation of our method and its application to concrete examples.

ABSTRACT. We consider some of the issues and trade-offs in computing useful interpolants in practice, including questions of proof search strategy, proof translation vs. local proof and interpolant optimization. These issues are explored empirically using the Duality fixed point engine as a platform and benchmark problems from software model checking.

ABSTRACT. The problem of reasoning automatically about string formulae, containing constraints such as string/word equations, regular language membership, or length restrictions, has increasingly received attention over the past years. Much of the existing work has concentrated on checking satisfiability of string formulae, by means of translation to bit-vector formulae or analysis of finite automata representations, among others. We report about ongoing research on Craig interpolation for string formulae, done in the context of work presented in our CAV’14 paper.

ABSTRACT. We consider the problem of verifying safety of a program in the absence of code for called procedures. Our goal is to synthesize maximal specifications of absent procedures that maintain safety of the given program. This is useful when the software to be verified contains calls to external components (e.g., libraries) that cannot be analyzed. Such components are usually (1) proprietary software whose source code is not available or (2) libraries that are too complex to be analyzed along with the client application. Thus, synthesized specifications can be used as stubs for calls to external components.

In this talk, we discuss a solution to this problem that relies on a reduction to a novel form of logical abduction, which we call generalized abduction. Generalized abduction is a powerful generalization of the classical abduction problem that allows us to abduce an individual specification (formula) for each unknown procedure — as opposed to a single formula in classical abduction. The fact that a procedure may be called from more than one call site, along with the interactions between different call sites, makes this problem quite challenging. We discuss the challenges faced when solving generalized abduction problems, present an algorithm for solving generalized abduction, and outline potential uses of interpolation as a way for solving this problem.

ABSTRACT. We present a method for interpolation based on DRUP proofs. Interpolants are widely used in model checking, synthesis and other applications. Most interpolation algorithms rely on a a resolution proof produced by a SAT-solver for unsatisfaible formulas. The proof is traversed and translated into an interpolant by replacing resolution steps with AND and OR gates. This process is efficient (once there is a proof) and generates interpolants that are linear in the size of the proof. As this method relies on the existence of a resolution proof, it depends on a SAT-solver that can log a resolution-proof.

In this work, we address three known weakness of this approach, due to its dependence on a resolution proof: (1) performance degradation experienced by the SAT-solver and the extra memory requirements needed when logging a resolution proof; (2) the proof generated by the solver is not necessarily the "best'' proof for interpolantion, and (3) combining proof logging with pre-processing is complicated. We show that these issues can be remedied by using DRUP proofs.

First, we show how to produce an interpolant from a DRUP proof, even when pre-processing is enabled. Then, we give a novel interpolation algorithm that produces interpolants partially in CNF. More precisely, our algorithm return the CNF component of the interpolant. In case that the proof permits it, the interpolant is a pure CNF. Lastly, we show how a DRUP proof can be reconstructed on-the-fly to yield better interpolants. Our reconstruction aims at maximizing the CNF componenet of the interpolant forcing a specific type of resolutions.

We implemented our DRUP-based interpolation framework in MiniSAT, and evaluated its affect using Avy - a SAT-based model checking algorithm that heavily relies on interpolation. We show the affect our method has on model checking and demonstrate the usefulness of our different heuristics.