Using Symmetries to Lift Satisfiability Checking

We analyze how symmetries can be used to compress structures (also known as interpretations) onto a smaller domain without loss of information. This analysis suggests the possibility to solve satisfiability problems in the compressed domain for better performance. Thus, we propose a 2-step novel method: (i) the sentence to be satisfied is automatically translated into an equisatisfiable sentence over a ``lifted'' vocabulary that allows domain compression; (ii) satisfiability of the lifted sentence is checked by growing the (initially unknown) compressed domain until a satisfying structure is found. The key issue is to ensure that this satisfying structure can always be expanded into an uncompressed structure that satisfies the original sentence to be satisfied. We present an adequate translation for sentences in typed first-order logic extended with aggregates. Our experimental evaluation shows large speedups for generative configuration problems. The method also has applications in the verification of software operating on complex data structures. Further refinements of the translation are left for future work.

Quantification and aggregation over concepts of the ontology

The first phase of developing an intelligent system is the selection of an ontology of symbols representing relevant concepts of the application domain. These symbols are then used to represent the knowledge of the domain. This representation should be \emph{elaboration tolerant}, in the sense that it should be convenient to modify it to take into account new knowledge or requirements. Unfortunately, current formalisms require a significant rewrite of that representation when the new knowledge is about the \emph{concepts} themselves: the developer needs to "\emph{reify}" them. This happens, for example, when the new knowledge is about the number of concepts that satisfy some conditions. The value of expressing knowledge about concepts, or "intensions", has been well-established in \emph{modal logic}. However, the formalism of modal logic cannot represent the quantifications and aggregates over concepts that some applications need. To address this problem, we developed an extension of first order logic that allows referring to the \emph{intension} of a symbol, i.e., to the concept it represents. We implemented this extension in IDP-Z3, a reasoning engine for FO($\cdot$) (aka FO-dot), a logic-based knowledge representation language. This extension makes the formalism more elaboration tolerant, but also introduces the possibility of syntactically incorrect formula. Hence, we developed a guarding mechanism to make formula syntactically correct, and a method to verify correctness. The complexity of this method is linear with the length of the formula. This paper describes these extensions, how their relate to intensions in modal logic and other formalisms, and how they allowed representing the knowledge of four different problem domains in an elaboration tolerant way.

IDP-Z3: a reasoning engine for FO

An important sign of intelligence is the capacity to apply a body of knowledge to a particular situation in order to not only derive new knowledge, but also to determine relevant questions or provide explanations. Developing interactive systems capable of performing such a variety of reasoning tasks for the benefits of its users has proved difficult, notably for performance and/or development cost reasons. Still, recently, a reasoning engine, called IDP3, has been used to build such systems, but it lacked support for arithmetic operations, seriously limiting its usefulness. We have developed a new reasoning engine, IDP-Z3, that removes this limitation, and we put it to the test in four knowledge-intensive industrial use cases. This paper describes FO(.) (aka FO-dot), the language used to represent knowledge in the IDP3 and IDP-Z3 system. It then describes the generic reasoning tasks that IDP-Z3 can perform, and how we used them to build a generic user interface, called the Interactive Consultant. Finally, it reports on the four use cases. In these four use cases, the interactive applications based on IDP-Z3 were capable of intelligent behavior of value to users, while having a low development cost (typically 10 days) and an acceptable response time (typically below 3 seconds). Performance could be further improved, in particular for problems on larger domains.