Abstract: Let us consider the following problem: Given a (probably huge) set of sets S and a query set q, is there some set s in S such that s is a subset of q? This problem occurs in at least four application areas: the matching of a large number (usually several 100,000s) of production rules, the processing of queries in data bases supporting set-valued attributes, the identification of inconsistent subgoals during artificial intelligence planning and the detection of potential periodic chains in labeled tableau systems for modal logics. In this paper, we introduce a data structure and algorithm that allow a compact representation of such a huge set of sets and an efficient answering of subset and superset queries. The algorithm has been used successfully in the IPP system and enabled this planner to win the ADL track of the first planning competition.
Abstract: We introduce mathematical programming and atomic decomposition as the basic modal (T-Box) inference techniques for a large class of modal and description logics. The class of description logics suitable for the proposed methods is strong on the arithmetical side. In particular there may be complex arithmetical conditions on sets of accessible worlds (role fillers). The atomic decomposition technique can deal with set constructors for modal parameters (role terms) and parameter (role) hierarchies specified in full propositional logic. Besides the standard modal operators, a number of other constructors can be added in a relatively straightforward way. Examples are graded modalities (qualified number restrictions) and also generalized quantifiers like `most', `n%', `more' and `many'.
Abstract: We investigate how to augment a given logical system, for example an arithmetical equation solver, with a Boolean component. The atomic decomposition technique proposed in this paper reduces reasoning about the Boolean component in the combined system to reasoning in the pure basic system only. A typical instance of this scheme is a linear programming system which is to be augmented with reasoning about cardinalities of sets, or other functions mapping sets to integers. The sets and their set-theoretic relationships are axiomatized with propositional logic. Atomic decomposition then reduces reasoning about numerical attributes of these sets to arithmetic equation solving.
Abstract: We introduce a new technique that translates cardinality information about finite sets into simple arithmetic terms and thereby enables a system to reason about such set cardinalities by solving arithmetic equation problems. The atomic decomposition technique separates a collection of sets into mutually disjoint smallest components (``atoms'') such that the cardinality of the sets are just the sum of the cardinalities of their atoms. With this idea it is possible to have languages combining arithmetic formulae with set terms, and to translate the formulae of this combined logic into pure arithmetical formulae. As a particular application we show how this technique yields new inference procedures for concept languages with so called number restriction operators.
Abstract: A key problem in case-based reasoning is the representation, organization and maintenance of case libraries. While current approaches rely on heuristic and psychologically inspired formalisms, terminological logics have emerged as a powerful representation formalism with clearly defined formal semantics. This paper demonstrates how the indexing of case libraries can be grounded on terminological logics by using them as a kind of query language to the case library. Indices of cases are represented as concepts in a terminological logic. They are automatically constructed from the symbolic representation of cases with the help of a well-defined abstraction process. The retrieval of cases from the library is grounded on concept classification.
Abstract: We describe reasoning methods for the interval-based modal temporal logic LLP which employs the modal operators sometimes, always, next, and chop. We propose a constraint deduction approach and compare it with a sequent calculus, developed as the basic machinery for the deductive planning system PHI which uses LLP as underlying formalism.