ARW-DT 2014 - AUTOMATED REASONING WORKSHOP/DEDUKTIONSTREFFEN PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. The effectiveness of interactive theorem provers (ITPs) has increased in a way that the bottleneck in the interactive process shifted from effectiveness to efficiency. Proving large theorems still needs a lot of effort for the user interacting with the system. This issue is recognized by the ITP-communities and improvements are being developed. However, in contrast to properties like soundness or completeness, where rigorous methods are applied to provide evidence, the evidence for a better usability is lacking in many cases. Our contribution is the application of methods from the human-computer-interaction (HCI) field to ITPs. We report on the application of focus groups to evaluate the usability of Isabelle/HOL and the KeY system. We apply usability evaluation methods in order to a) detect usability issues in the interaction between ITPs and their users, and b) to analyze whether methods such as focus groups are applicable to the field of ITP.

ABSTRACT. We developed a method that allows to check the satisfiability of a formula in the combined theories of sets and the bridging functions card, sum, avg, min, max by using a prover for linear arithmetic. Since abstractions of certain verification task lie in this fragment, this method can be used for checking the behaviour of a program.

ABSTRACT. In the ForMaRE project formal mathematical reasoning is applied to economics. After an initial exploratory phase, it focused on auction theory and has produced, as its first results, formalized theorems and certified executable code.

ABSTRACT. Regression verification is an approach to prevent regressions in software development using formal verification. The goal is to prove that two versions of a program behave equally or differ in a specified way. We worked on an approach for regression verification, extending Strichman and Godlin's work by relational equivalence and two ways of using counterexamples.

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. 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.

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. 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. 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. 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. 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. WWe 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. 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. Motivated by the theory of relations on graphs and applications to spatial reasoning, we present a bi-intuitionistic logic BISKT with tense operators. The logic is shown to be decidable and have the effective finite model property. We present a sound, complete and terminating tableau calculus for the logic and use the MetTeL system to generate an implementation.

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

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. 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.