LEARNING FEATURES OF INTERMEDIATE COMPLEXITY FOR THE RECOGNITION OF BIOLOGICAL MOTION (2009)
Gamailiel Rodrigo, Sigala Alanís, Martin Giese
Abstract- Humans can recognize biological motion (e.g. a walker) from stimuli with impoverished information, like point-light displays (e.g. a “point-like walker”). Although the neural mechanism...
Hilbert’s ɛ-Terms in Automated Theorem Proving (2008)
Martin Giese, Wolfgang Ahrendt
Abstract. ɛ-terms, introduced by David Hilbert [8], have the form ɛx.φ, where x is a variable and φ is a formula. Their syntactical structure is thus similar to that of a quantified formulae, but...
Abstract UITP 2003 Preliminary Version Taclets (2008)
We give a short overview of the KeY prover – which is the proof system belonging to the KeY tool [1] – from a user interface perspective. In particular, we explain the concept of taclets, which...
Learning Based Representation of Complex Movement Patterns (2008)
The Problem: Development of theoretical methods for the representation of complex movements based on learned prototypical examples for technical applications, and as basis to understand action...
Saturation up to Redundancy for Tableau and Sequent Calculi (2008)
Abstract. We discuss an adaptation of the technique of saturation up to redundancy, as introduced by Bachmair and Ganzinger [1], to tableau and sequent calculi for classical first-order logic. This...
Towards Practical Reflection for Formal Mathematics (2008)
Martin Giese, Bruno Buchberger
Abstract. We describe a design for a system for mathematical theory exploration that can be extended by implementing new reasoners using the logical input language of the system. Such new reasoners...
zur Erlangung des Grades eines Doktors (2008)
Der Naturwissenschaften, Der Fakultät Für, Der Medizinischen Fakultät, Theresa Cooke, Prüfungskommission Prof, ...
und
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2008)
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
Taclets and the KeY Prover Extended Abstract (2008)
Abstract. We give a short overview of the KeY prover, which is the proof system belonging to the KeY tool [1], from a user interface perspective. In particular, we explain the concept of taclets...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
Abstract KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz
2, Wolfram Menzel 1, and Peter H. Schmitt 1 1
The Approach: Integrating Object Oriented Design and Formal Veri cation (2007)
Wolfgang Ahrendt Thomas, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
. This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verication. A distinctive feature of our approach is...
Abstract. There is an increasing number of publications in which the analytic tableaux calculus is combined with technology based on constraint solving. Although the details, as well as the purpose...
Estimation of Skill Levels in Sports based on Hierarchical Spatio-Temporal Correspondences (2007)
Winfried Ilg, Johannes Mezger, Martin Giese
We present a learning-based method for the estimation of skill levels from sequences of complex movements in sports. Our method is based on a hierarchical algorithm for computing spatio-temporal...
Abstract. We present a calculus that integrates equality handling by superposition into a free variable tableau calculus. We prove completeness of this calculus by an adaptation of the model...
FASE System Description The System: Integrating Object-Oriented Design and Formal Methods ⋆ (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Position Paper: Proof Search without Backtracking using Instance Streams (2007)
Most existing automated proof procedures using free-variable analytic tableaux require iterative deepening and backtracking to guarantee completeness. The general process for closing a proof with,...
A First-order Simplication Rule with Constraints (2007)
Abstract. Several variants of a rst-order simplication rule for nonnormal form tableaux using syntactic constraints are presented. These can be used as a framework for porting renements of clausal...
Position Paper: Proof Search without Backtracking using Instance Streams (2007)
Most existing automated proof procedures using free-variable analytic tableaux require iterative deepening and backtracking to guarantee completeness. The general process for closing a proof with,...
Hilbert's -terms in Automated Theorem Proving (2007)
Martin Giese, Wolfgang Ahrendt
Abstract. #-terms, introduced by David Hilbert [8], have the form #x.#, where x is a variable and # is a formula. Their syntactical structure is thus similar to that of a quantified formulae, but...
Abstract UITP 2003 Preliminary Version Taclets (2007)
We give a short overview of the KeY prover – which is the proof system belonging to the KeY tool [1] – from a user interface perspective. In particular, we explain the concept of taclets, which...
Abstract. There is an increasing number of publications in which the analytic tableaux calculus is combined with technology based on constraint solving. Although the details, as well as the purpose...
Technical Report no. 2003-05 The KeY Tool 1 (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2007)
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
Model generation style completeness proofs for constraint tableaux with superposition. (2007)
We present several calculi that integrate equality handling by superposition and ordered paramodulation into a free variable tableau calculus. We prove completeness of this calculus by an adaptation...
Giese, Martin, Schoenegge, Arno
Georg Cantor in 1895 gave the first (informal) proof for the fact that any two countable, densely ordered sets without endpoints are isomorphic. Here we report on a fully formal proof of this fact...
KIV zur Verifikation von ASM-Spezifikationen am Beispiel der DLX-Pipelining Architektur. (2007)
Giese, Martin, Kempe, David, Schoenegge, Arno
In der hier beschriebenen Fallstudie wurde das KIV-System (Karlsruhe Interactive Verifier) zur Verifikation von ASM-Spezifikationen (Abstract State Machines) eingesetzt. Diese Fallstudie behandelt...
Predicting point-light actions in real-time (2007)
Graf, Markus, Reitzner, Bianca, Corves, Caroline, Casile, Antonino, Giese, Martin, Prinz, Wolfgang
Predicting poitn-light actions in real-time (2007)
Graf, Markus, Reitzner, Bianca, Corves, Caroline, Casile, Antonino, Giese, Martin, Prinz, Wolfgang
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
Martin Giese, Tudor Jebelean (eds, B. Buchberger, R. Hemmecke, T. Jebelean, M. Kauers, ...
Many groups around the world conduct research on formal methods for software development, and in most of these groups, some of the effort goes into the problem of reasoning about loops. There is of...
Temur Kutsia, Mircea Marin (eds, B. Buchberger, R. Hemmecke, T. Jebelean, M. Kauers, ...
aim at strengthening cooperation between the research groups at the Research
Towards practical reflection for formal mathematics (2007)
Martin Giese, Bruno Buchberger
Abstract. We describe a design for a system for mathematical theory exploration that can be extended by implementing new reasoners using the logical input language of the system. Such new reasoners...
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Bubel, Richard, Giese, Martin, Hähnle, Reiner, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Predicting point-light actions (2005)
Graf, Markus, Giese, Martin, Casile, Antonino, Prinz, Wolfgang
Simplifying transformations of OCL constraints (2005)
Abstract. With the advent of Model Driven Architecture, OCL constraints are no longer necessarily written by humans. They can be part of models that emerge from a chain of transformations. They might...
A calculus for type predicates and type coercion (2005)
Abstract. We extend classical first-order logic with subtyping by type predicates and type coercion. Type predicates assert that the value of a term belongs to a more special type than the signature...
Learning features of intermediate complexity for the recognition of biological motion (2005)
Rodrigo Sigala, Thomas Serre, Tomaso Poggio, Martin Giese
Abstract. Humans can recognize biological motion from strongly impoverished stimuli, like point-light displays. Although the neural mechanism underlying this robust perceptual process have not yet...
Simplifying transformations of OCL constraints (2005)
Abstract. With the advent of Model Driven Architecture, OCL constraints are no longer necessarily written by humans. They can be part of models that emerge from a chain of transformations. They might...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2004)
Bernhard Beckert, Bernhard Beckert, Martin Giese, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
In Formal Methods for Open Object-Based Distributed Systems (2004)
Abb Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
[AdB90] Pierre America and Frank de Boer. Proving total correctness of recursive procedures. Information and Computation, 84(2):129– 162, 1990. [AdB94] Pierre America and Frank de Boer. Reasoning...
Rule-based Simplification of OCL Constraints (2004)
Abstract. To help designers in writing OCL constraints, we have to construct systems that can generate some of these constraints. This might be done by instantiating templates, by combining...
Johannes Mezger, Winfried Ilg, Martin Giese (2004)
Email Mezger Gris, Johannes Mezger, Winfried Ilg, Martin Giese, Graphisch-interaktive Systeme, ...
We present an extension to a previous morphing method for human motion. It works on motion capture data that is segmented into movement elements. Our new timewarping algorithm accepts time-dependent...
Rule-based Simplification of OCL Constraints (2004)
Martin Giese, Reiner Hähnle, Daniel Larsson
Abstract. To help designers in writing OCL constraints, we have to construct systems that can generate some of these constraints. This might be done by instantiating templates, by combining...
From informal to formal specifications in UML (2004)
Abstract. In this paper, we consider a way of bridging informal and formal specification. Most projects have a need for an informal description of the requirements of the system which all people...
Rule-based Simplification of OCL Constraints (2004)
Martin Giese, Reiner Hähnle, Daniel Larsson
Abstract. To help designers in writing OCL constraints, we have to construct systems that can generate some of these constraints. This might be done by instantiating templates, by combining...
Oslo, 2003 • The KeY system: Integrating object-orientated design and formal (2003)
Martin Giese, W. Ahrendt, T. Baar, B. Beckert, M. Giese, ...
• Incremental Closure is a proof search method developed in the context of the KeY project • The purpose of the KeY project: Integrate formal software specification and verification into...
Simplification rules for constrained formula tableaux (2003)
Abstract. Several variants of a first-order simplification rule for nonnormal form tableaux using syntactic constraints are presented. These can be used as a framework for porting methods like unit...
There is an increasing number of publications in which the analytic tableaux calculus is combined with technology based on constraint solving. Although the details, as well as the purpose of these...
Simplification Rules for Constrained Formula Tableaux (2003)
Several variants of a first-order simplification rule for nonnormal form tableaux using syntactic constraints are presented. These can be used as a framework for porting methods like unit resolution...
Proof search without backtracking for free variable tableaux / (2002)
Karlsruhe, University, Diss., 2002 (Nur beschränkt für den Austausch).
Incremental closure of free variable tableaux (2001)
Abstract. This paper presents a technique for automated theorem proving with free variable tableaux that does not require backtracking. Most existing automated proof procedures using free variable...
Incremental closure of free variable tableaux (2001)
Abstract. This paper presents a technique for automated theorem proving with free variable tableaux that does not require backtracking. Most existing automated proof procedures using free variable...
A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition (2001)
We present a calculus that integrates equality handling by superposition into a free variable tableau calculus. We prove completeness of this calculus by an adaptation of the model generation [1, 15]...
Model Generation Style Completeness Proofs for Constraint Tableaux with Superposition (2001)
We present several calculi that integrate equality handling by superposition and ordered paramodulation into a free variable tableau calculus. We prove completeness of this calculus by an adaptation...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
A first-order simplification rule with constraints (2000)
Abstract. Several variants of a first-order simplification rule for non-normal form tableaux using syntactic constraints are presented. These can be used as a framework for porting refinements of...
Proof search without backtracking using instance streams, position paper (2000)
Most existing automated proof procedures using free-variable analytic tableaux require iterative deepening and backtracking to guarantee completeness. The general process for closing a proof with,...
A first-order simplification rule with constraints (2000)
Abstract. Several variants of a first-order simplification rule for non-normal form tableaux using syntactic constraints are presented. These can be used as a framework for porting refinements of...
The KEY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
The KeY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
Abstract This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive...
Fakultat Fur Informatik, Martin Giese, Martin Giese, Arno Schönegge, Arno Schonegge
Georg Cantor in 1895 gave the first (informal) proof for the fact that any two countable, densely ordered sets without endpoints are isomorphic [1]. Here we report on a fully formal proof of this...
Mit 4 Taf. in: Zeitschrift f. wiss. Zool. Bd 114.