Proving Compiler Correctness with Evolving Algebra (2008)
Speci Cations, Bernhard Beckert, Reiner Hahnle
The purpose of this note is to de ne a framework for proving compiler correctness with evolving algebra (EA) speci cations [2]. Although our speci c domain is the veri cation of a Prolog-to-
The Tableau-based Theorem Prover (2007)
Version Bernhard Beckert, Bernhard Beckert, Reiner Hahnle, Peter Oel, Martin Sulzmann
This paper gives an overview of the system with a special focus on the new features of 3 T A P Version 4.0, including: efficient completion-based equality reasoning, methods for handling redundant...
Bernhard Beckert, Reiner Hahnle, Gonzalo Escalada-imaz
We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of antilinks....
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...
Reiner Hahnle, Project M. D'agostino, J. Dix, I. Gent, M. Kummer, J. Lu, ...
This book is a revised version of my PhD thesis, submitted to the Department
Towards an e cient Tableau Proof Procedure for Multiple-Valued Logics (2007)
One of the obstacles against the use of tableau-based theorem provers for non-standard logics is the ine ciency of tableau systems in practical applications, though they are highly intuitive and...
Deduction by Combining Semantic Tableaux and Integer Programming (2007)
Bernhard Beckert, Reiner Hahnle
Abstract. In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated...
Deduction by Combining Semantic Tableaux and Integer Programming (2007)
Bernhard Beckert, Reiner Hahnle
Abstract. In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated...
Institute for Logic, Complexity, and Deduction Systems (2007)
Bernhard Beckert, Reiner Hahnle, Neil V. Murray, Anavai Ramesh
Manipulation of Boolean functions has important applications in such fields as hardware verification, non-monotonic reasoning, and decision support. Most often, in such applications, the set of prime...
Bernhard Beckert, Reiner Hahnle, Gonzalo Escalada-imaz
Abstract. We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of...
Bernhard Beckert, Reiner Hahnle, Peter Oel, Martin Sulzmann
3 T A P is a tableau-based theorem prover for many-valued first-order logics with sorts (in the two-valued version with equality); it is implemented in Prolog. This paper gives an overview of the...
Institute for Logic, Complexity, and Deduction Systems (2007)
Anavai Ramesh, Neil V. Murray, Bernhard Beckert, Reiner Hahnle
In [11] Reiter laid the foundations of the formal theory of an approach to diagnosis known as diagnosis from first principles. His work was based on the work of many researchers, notably that of de...
Anavai Ramesh, Bernhard Beckert, Reiner Hahnle, Neil V. Murray
Abstract. The concept of anti-link is defined (an anti-link consists of two occurrences of the same literal in a formula), and useful equivalence-preserving operations based on anti-links are...
A Theorem Proving Approach to Analysis of Secure Information Flow* (2005)
Adam Dravas, Ádám Darvas, David Sands, Reiner Hahnle, David S
Most attempts at analysing secure information flow in programs are based on domain-specific logics. Though computationally feasible, these approaches su#er from the need for abstraction and the high...
The KeY system allows integrated informal and formal development of objectoriented Java software. In this paper we report on a major industrial case study involving safety-critical software for...
An authoring tool for informal and formal requirements specifications (2002)
Reiner Hahnle, Kristofer Johannisson, Aarne Ranta
Abstract We describe foundations and design principles of a tool that supports authoring of informal and formal software requirements specifications simultaneously and from a single source. The tool...
Complexity of many-valued logics (2001)
Like in the case of classical logic and other non-standard logics, a variety of complexity-related questions can be asked in the context of many-valued logic. Some questions,
Connecting OCL with the rest of the world (2001)
Abstract The paper addresses the problems of making program specifications written in OCL easier to read and to maintain. The solution proposed grammar of specifications with translations into OCL,...
A modular reduction of regular logic to classical logic (2001)
Ramon Bejar, Reiner Hahnle, Felip Manya
In this paper we first define a reduction that transforms an instance of Regular-SAT into a satisfiability equivalent instance of SAT. The reduction has interesting properties: (i) the size of is...
An integrated metamodel for OCL types (2000)
Abstract The main objectives of OCL are to restrict UML models by additional constraints and to clarify the denition of the UML meta model. For certain applications, however, it is crucial for the...
The 2-SAT problem of regular signed CNF formulas (2000)
Bernhard Beckert, Reiner Hahnle, Felip Manya
Signed conjunctive normal form (signed CNF) is a classical conjunctive clause form using a generalized notion of literal, called signed atom. A signed atom is an expression of the form S: p, where p...
Transformations between signed and classical clause logic (1999)
Bernhard Beckert, Reiner Hahnle
Abstract. In the last years two automated reasoning techniques for clause normal form arose in which the use of labels are prominently featured: signed logic and annotated logic programming, which...
ESSLLI 1998 COURSE Tableau-Based Theorem Proving (1998)
is allowed only with permission. The preliminary nature of this document entails that it has not been proof read by anyone else besides the author. The reader is advised to be aware of errors and...
Fast subsumption checks using anti-links (1997)
Interner Bericht, Fakultat Fur Informatik, Anavai Ramesh, Anavai Ramesh, Neil V. Murray, Neil V. Murray, ...
This report has been submitted for publication elsewhere, and will be copyrighted if accepted.
Bernhard Beckert, Reiner Hahnle
Abstract. We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of...
Bernhard Beckert and Reiner Hahnle (1997)
Bernhard Beckert, Reiner Hahnle, Gonzalo Escalada-imaz
. We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of anti-links....
Common Syntax of the DFGSchwerpunktprogramm Deduction (1996)
Reiner Hahnle, Fakultat Fur Informatik, Manfred Kerber, Christoph Weidenbach, Im Stadtwald
A common exchange format for logic problems to be used by members of the DFG-Schwerpunktprogramm "Deduktion " is introduced. It is thought to be an internal format that can easily...
Common Syntax of the DFG-Schwerpunktprogramm "Deduktion" (1996)
Reiner Hähnle, Reiner Hahnle, Fakultat Fur Informatik, Manfred Kerber, Manfred Kerber, Christoph Weidenbach, ...
A common exchange format for logic problems to be used by members of the DFG-Schwerpunktprogramm "Deduktion" is introduced. It is thought to be an internal format that can easily be parsed...
Interner Bericht, A-ordered Tableaux, Reiner Hähnle, Reiner Hahnle, Stefan Klingenbeck, Stefan Klingenbeck
In resolution proof procedures refinements basedon A-orderings of literals havea long tradition and are well investigated. In tableau proof proceduressuch refinements were only recently introduced by...
Semantic tableaux with ordering restrictions (1994)
Stefan Klingenbeck, Reiner Hahnle
Abstract. The aim of this paper is to make restriction strategies based on orderings of the Herbrand universe available for semantic tableau-like calculi as well. A marriage of tableaux and ordering...
Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics (1990)
One of the obstacles against the use of tableau-based theorem provers for non-standard logics is the inefficiency of tableau systems in practical applications, though they are highly intuitive and...