previous day
all days

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 181A: PRIVACY, SAT
Location: FH, Hörsaal 3
Defining privacy is supposed to be easy
SPEAKER: Luca Viganò

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

Extended Resolution in Modern SAT Solving

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.

10:15-10:45Coffee Break
10:45-13:15 Session 183D: Planning, Deontic Logic, Herbrand
Location: FH, Hörsaal 3
Using CSP Meta Variables in AI Planning
SPEAKER: Mark Judge

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.

Automated Reasoning in Deontic Logic
SPEAKER: unknown

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.

(AI) Planning to Reconfigure your Robot?
SPEAKER: Mark Judge

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.

Second-Order Characterizations of Definientia in Formula Classes

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.

On Herbrand theorems for classical and non-classical logics

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.

13:00-14:30Lunch Break
14:30-16:00 Session 185A: Non-Classical Ontologies I
Location: FH, Hörsaal 3
Models Minimal Modulo Subset-Simulation for Expressive Propositional Modal Logics
SPEAKER: unknown

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.

A Resolution-Based Prover for Normal Modal Logics

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.

Computing Uniform Interpolants of ALCH-Ontologies with Background Knowledge
SPEAKER: unknown

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.

16:00-16:30Coffee Break
16:30-18:00 Session 187A: Non-Classical Ontologies II: Higher-Order
Location: FH, Hörsaal 3
The Leo-III Project
SPEAKER: unknown

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.

Socratic Proofs for Propositional Linear-Time Logic
SPEAKER: unknown

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

Modular Verification of Interconnected Families of Uniform Linear Hybrid Automata

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.