ABSTRACT. Formally specifying privacy goals is not trivial. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. A subtle question is how we can be sure that we have specified all pairs of worlds to properly reflect our intuitive privacy goal. To address this problem, we introduce in this paper a novel and declarative way to specify privacy goals, called `privacy', and relate it to static equivalence. This new approach is based on specifying two formulae E1 and E2 in first-order logic with Herbrand universes, where E1 reflects the intentionally released information and E2 includes the actual cryptographic (`technical') messages the intruder can see.

Then E1-E2 privacy means that the intruder cannot derive any `non-technical' statement from E2 that he cannot derive from E1 already. We describe by a variety of examples how this notion can be used in practice. Even though E1-E2 privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the specifications that are currently used in verification tools, and obtain partial tool support for E1-E2 privacy.

Joint work with Sebastian Moedersheim and Thomas Gross

ABSTRACT. Modern SAT solvers are applied in many academic and industrial fields. The used CDCL algorithm is based on resolution, but solvers also use stronger reasoning techniques in preprocessing steps. Only few attempts have been made to include stronger reasoning techniques into the search itself. The current work revisits the embedding of extended resolution into SAT solvers, and improves existing work. Experiments indicate that the approach is very promising.

ABSTRACT. Reformulating Artificial Intelligence Planning problems as Constraint Satisfaction Problems(CSPs) brings a number of benefits. In this reformulation process however, the structure of the original planning problem is lost. Therefore, no planning problem specific guidance may be used during the assignment of values to the CSP variables. Extending work, in which we implemented a planning-specific CSP variable and value selection heuristic, the work described here aims to make better use of the propagation inherent in a given CSP solver by using CSP meta variables. Such meta variables are used here for goal-locking and for the assignment of resources to tasks within the problem solution process, with the aim being to reduce the search space, and to better guide the search within it.

ABSTRACT. Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are discussed for different applications like argumentation theory, legal reasoning and actions in multi-agent systems. Recently there also is growing interest in modelling human reasoning and testing the models with psychological findings. Deontic logic is an obvious tool to this end, because norms and licenses in human societies can be described easily. This paper concentrates on automated reasoning in deontic logic. We show that deontic logic can be translated into the description logic ALC, for which the first oder reasoning system Hyper offers a decision procedure.

ABSTRACT. Current and future robotics and autonomous system applications will be used in highly complex environments. In such situations, automatic reconfiguration, due either to changing requirements or equipment failure, is highly desirable. By using a model of autonomy based around the Robot Operating System (ROS), and building on previous work, it is possible to use Artificial Intelligence (AI) Planning to facilitate the automatic reconfiguration. In this way, standard AI Planning machinery may be used with a suitable mathematical model of a given system. This paper reviews the background to this concept and details the initial steps taken towards the combination of AI Planning technology and a physical system, with the aim being to have the planner provide possible validated system reconfigurations which can then be implemented on the hardware.

ABSTRACT. For a given formula, a definiens in terms of a given set of predicates can be characterized quite straightforwardly with predicate quantification. Methods for second-order quantifier elimination and the closely related computation of forgetting, projection and uniform interpolants can then be applied to compute such definientia. Here we address the question, whether also definientia that are in given classes of formulas, such as Horn formulas, conjunctions of atoms or Krom formulas, can be specified with predicate quantification and can thus be computed by second-order quantifier elimination methods.

ABSTRACT. The talk is devoted to Herbrand-type theorems for an enough wide spectrum of first-order logics for both the classical and intuitionistic cases as well as for their modal extensions. A way for the construction of Herbrand theorems for first-order logics containing the ineliminable cut rule is discussed.

ABSTRACT. Terminating procedures for the generation of models minimal modulo subset-simulation for normal modal logics have recently been presented. In this abstract we explain what are the challenges to generalise those procedures to more expressive modal logics, and discuss possible solutions.

ABSTRACT. We present a prototype tool for automated reasoning for multimodal normal logics where combinations of the axioms K, T, D, B, 4, and 5 hold. The theorem prover is based on previous work on resolution calculi for such logics. We briefly present the syntax, the semantics, and the calculus for the basic normal logic together with the inference rules for dealing with each specific axiom. We then give details of the implementation of the prover and discuss future work.

ABSTRACT. Uniform interpolation is a technique to restrict the concept and roles symbols used in an ontology to a specified subset, while preserving all logical entailments that can be expressed using that subset. We propose the notion of relative uniform interpolation, where knowledge from a second ontology is taken into account, and present a method for the description logic ALCH. Relative uniform interpolation of ontologies corresponds to strongest necessary conditions of formulae studied in classical logics.

ABSTRACT. We report on the recently started Leo-III project, in which we design and implement a state-of-the-art Higher-Order Logic Theorem Prover, the successor of the well known LEO-II prover. Leo-III will be based on ordered paramodulation/superposition. In constrast to LEO-II, we replace the internal term representation (the commonly used simply typed lambda calculus) by a more expressive system supporting type polymorphism. In the course of the project, we plan to further enhance the type system with type classes and type constructors similar to System F ω . In order to achieve a substantial performance speed-up, the architecture of Leo-III will be based on massive parallelism (e.g. And/Or-Parallelism, Multisearch). The current design is a multi-agent blackboard archi- tecture that will allow to independently run agents with our proof calculus as well as agents for external (specialized) provers. Leo-III will focus right from the start on compatibility to the widely used TPTP infrastructure . Moreover, it will offer built-in support for specialized external prover agents and provide external interfaces to interactive provers such as Isabelle/HOL . The implementation will excessively use term sharing and several indexing techniques . Leo-III will also offer special support for reasoning in various quantified non-classical logics by exploiting a semantic embedding approach.

ABSTRACT. This paper presents a calculus of Socratic proofs for Propositional Linear-Time Logic (PLTL) and discuss potential automation of its proof search.

ABSTRACT. We provide a mathematical model for unbounded parallel compositions of structurally similar linear hybrid automata, whose topology and flows are described using parametrized formulas. We study how the analysis of safety properties for the overall system can be performed hierarchically, using quantifier elimination to derive conditions on the parameters of individual components.