Specification Predicates with Explicit Dependency Information (2009)
Richard Bubel, Reiner Hähnle, Peter H. Schmitt
Abstract. Specifications of programs use auxiliary symbols to encapsulate concepts for a variety of reasons: readability, reusability, structuring and, in particular, for writing recursive...
Symbolic Fault Injection (2009)
Abstract. Fault tolerance mechanisms are a key ingredient of dependable systems. In particular, software-implemented hardware fault tolerance (SIHFT) is gaining in popularity, because of its cost...
Symbolic Fault Injection (2009)
Abstract. Fault tolerance mechanisms are a key ingredient of dependable systems. In particular, software-implemented hardware fault tolerance (SIHFT) is gaining in popularity, because of its cost...
A Dynamic Logic for Deductive Verification of C Programs with KeY-C (2009)
Oleg Mürk, Daniel Larsson, Reiner Hähnle
Abstract. We present KeY-C: a tool for deductive verification of C programs. KeY-C allows verification of C programs w.r.t. operation contracts and invariants. It is based on an earlier version of...
Abstract Hoare Logic with Updates A Hoare-Style Calculus with Explicit State Updates (2008)
We present a verification system for a variant of Hoare-logic that supports proving program correctness by forward symbolic execution. No explicit weakening rules are needed and first-order reasoning...
A Dynamic Logic for Deductive Verification of C Programs with KeY-C (2008)
Oleg Mürk, Daniel Larsson, Reiner Hähnle
Abstract. We present KeY-C: a tool for deductive verification of C programs. KeY-C allows verification of C programs w.r.t. operation contracts and invariants. It is based on an earlier version of...
Abstract A Hoare-Style Calculus with Explicit State Updates (2008)
We present a verification system for a variant of Hoare-logic that supports proving by forward symbolic execution. In addition, no explicit weakening rules are needed and first-order reasoning is...
Ádám Darvas, Reiner Hähnle, David Sands
Most attempts at analysing secure information flow in programs are based on domainspecific logics. Though computationally feasible, these approaches suffer from the need for abstraction and the high...
Symbolic Fault Injection (2008)
Daniel Larsson, Reiner Hähnle, Daniel Larsson, Reiner Hähnle
Abstract. Computer systems that are dependable in the presence of faults are increasingly in demand. Among available fault tolerance mechanisms, software-implemented hardware fault tolerance (SIHFT)...
Jing Pan, Reiner Hähnle, Reiner Hähnle
ii We present a theorem proving approach to analysis of secure information flow using the technique of inspecting failed proofs and open goals. We then introduce an approximate interpretation of...
Verification by Parallelization of Parametric Code ⋆ (2008)
Abstract. Loops and other unbound control structures constitute a major bottleneck in formal software verification, because correctness proofs over such control structures generally require user...
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...
Verification by Parallelization of Parametric Code ⋆ (2008)
Abstract. Loops and other unbound control structures constitute a major bottleneck in formal software verification, because correctness proofs over such control structures generally require user...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the...
Study Key System, Richard Bubel, Reiner Hähnle
The date of receipt and acceptance will be inserted by the editor Abstract. The KeY system allows integrated informal and formal development of object-oriented JAVA software. In this paper we report...
Introduction Deductive Software Verification (2008)
Deductive Software Verification is a formal technique for reasoning about properties of programs. It has been around 1 for nearly 40 years, however, a number
Symbolic Fault Injection (2008)
Abstract. Computer systems that are dependable in the presence of faults are increasingly in demand. Among available fault tolerance mechanisms, software-implemented hardware fault tolerance (SIHFT)...
Linearity and Regularity with Negation Normal Form ∗ (2008)
Reiner Hähnle, Neil V. Murray, Erik Rosenthal
Proving completeness of NC-resolution under a linear restriction has been elusive; it is proved here for formulas in negation normal form. The proof uses a generalization of the Anderson-Bledsoe...
Deductive Verification of C Programs with KeY-C (2008)
Oleg Mürk, Daniel Larsson, Reiner Hähnle
Abstract. We present KeY-C: a tool for deductive verification of C programs. KeY-C allows verification of C programs w.r.t. operation contracts and invariants. It is based on an earlier version of...
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...
KeY: A Formal Method for Object-Oriented Systems (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented...
Bernhard Beckert, Reiner Hähnle, 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...
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...
Chapter 1 THE SAT PROBLEM OF SIGNED CNF FORMULAS (2008)
Bernhard Beckert, Reiner Hähnle, Felip Manyà
Abstract Signed conjunctive normal form (signed CNF) is a classical conjunctive clause form using a generalised notion of literal, called signed literal. A signed literal is an expression of the form...
Propositional Non Clausal Deduction and Diagnosis (2008)
Anavai Ramesh, Neil V. Murray, Bernhard Beckert, Reiner Hähnle
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...
The Even More Liberalized δ-Rule in Free Variable Semantic Tableaux (2008)
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
. In this paper we have a closer look at one of the rules of the tableau calculus presented in [3], called the ffi--rule, and the modification of this rule, that has been proved to be sound and...
Workshop Program 5th International Verification Workshop – VERIFY’08 (2008)
Bernhard Beckert, Gerwin Klein (chairs, Bernhard Beckert, Bernhard Beckert, Gerwin Klein, ...
The VERIFY workshop series aims at bringing together people who are interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem...
Some Remarks on Completeness, Connection Graph Resolution and Link Deletion (2007)
Reiner Hähnle, Neil V. Murray, Erik Rosenthal
A new completeness proof that generalizes the Anderson-Bledsoe excess literal argument is developed for connection-graph resolution. This technique also provides a simplified completeness proof for...
Semantic Semantic Tableaux (2007)
. Hyper tableaux and tableaux with selection function are combined to form a family of very general, saturation-based tableau calculi. Besides its generality, one benefit is a simple and uniform...
Fair Constraint Merging Tableaux in Lazy Functional Programming Style (2007)
Reiner Hähnle, Niklas Sörensson
Abstract. Constraint merging tableaux maintain a system of all closing substitutions of all subtableau up to a certain depth, which is incrementally increased. This avoids backtracking as necessary...
Unit Preference for Ordered Resolution and for Connection Graph Resolution (2007)
Reiner Hähnle, Neil V. Murray, Erik Rosenthal
Abstract. Strong completeness, which is almost automatic at the ground level for the tableau method and for path dissolution, is a question for many path-based calculi, most notably for...
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...
Fair Constraint Merging Tableaux in Lazy Functional Programming Style (2007)
Reiner Hähnle, Niklas Sörensson
Constraint merging tableaux maintain a system of all closing substitutions of all subtableau up to a certain depth, which is incrementally increased. This avoids backtracking as necessary in...
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...
The many-valued theorem prover 3TAP. 3rd. edition. (2007)
Hähnle, Reiner, Beckert, Bernhard, Gerberding, Stefan
This is the 3TAP handbook. 3TAP is a many-valued tableau-based theorem prover developed at the University of Karlsruhe. The handbook serves a triple purpose: first, it documents the history and...
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...
On the integration of security type systems into program logics (2007)
Reiner Hähnle, Jing Pan, Dennis Walter
Abstract. Type systems and program logics are often conceived to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring...
KeY-C: A tool for verification of C programs (2007)
Oleg Mürk, Daniel Larsson, Reiner Hähnle
Abstract. We present KeY-C, a tool for deductive verification of C programs. KeY-C allows to prove partial correctness of C programs relative to pre- and postconditions. It is based on a version of...
KeY-C: A tool for verification of C programs (2007)
Oleg Mürk, Daniel Larsson, Reiner Hähnle
Abstract. We present KeY-C, a tool for deductive verification of C programs. KeY-C allows to prove partial correctness of C programs relative to pre- and postconditions. It is based on a version of...
On the integration of security type systems into program logics (2007)
Reiner Hähnle, Jing Pan, Dennis Walter
Abstract. Type systems and program logics are often conceived to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring...
Generating unit tests from formal proofs (2007)
Christian Engel, Reiner Hähnle
Abstract. We present a new automatic test generation method for JAVA CARD based on attempts at formal verification of the implementation under test (IUT). Self-contained unit tests in JUnit format...
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...
On the integration of security type systems into program logics (2007)
Type systems and program logics are often conceived to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring...
Automating verification of loops by parallelization (2006)
Abstract. Loops are a major bottleneck in formal software verification, because they generally require user interaction: typically, induction hypotheses or invariants must be found or modified by...
Automating verification of loops by parallelization (2006)
Abstract. Loops are a major bottleneck in formal software verification, because they generally require user interaction: typically, induction hypotheses or invariants must be found or modified by...
Christian Engel, Responsible Supervisor, Prof Dr, Peter H. Schmitt, Supervisor Prof, Dr. Reiner Hähnle, ...
At this place I would like to thank everyone who supported me in creation of this thesis. First of all, I am very grateful to Prof. Dr. Peter H. Schmitt and Prof. Dr. Reiner Hähnle for their...
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...
OCL and Model Driven Engineering (2005)
Bézivin, Jean, Baar, Thomas, Gardner, Tracy, Gogolla, Martin, Hähnle, Reiner, Hussmann, Heinrich, ...
Precise modeling is essential to the success of the OMG's Model Driven Architecture initiative. At the modeling level (M1) OCL allows for the precision needed to write executable models. Can OCL be...
Reiner Hähnle, Jing Pan, Dennis Walter, Reiner Hähnle, Jing Pan, Dennis Walter, ...
Abstract. Type systems and program logics are often conceived to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring...
Normal forms for knowledge compilation (2005)
Reiner Hähnle, Neil V. Murray, Erik Rosenthal
Abstract. A class of formulas called factored negation normal form is introduced. They are closely related to BDDs, but there is a DPLL-like tableau procedure for computing them that operates in...
A theorem proving approach to analysis of secure information flow (2005)
Ádám Darvas, Reiner Hähnle, David S
Abstract. Most attempts at analysing secure information flow in programs are based on domain-specific logics. Though computationally feasible, these approaches suffer from the need for abstraction...
Normal forms for knowledge compilation (2005)
Reiner Hähnle, Neil V. Murray, Erik Rosenthal
Abstract. A class of formulas called factored negation normal form is introduced. They are closely related to BDDs, but there is a DPLL-like tableau procedure for computing them that operates in...
Verification of safety properties in the presence of transactions (2005)
Reiner Hähnle, Wojciech Mostowski
Abstract. The JAVA CARD transaction mechanism can ensure that a sequence of statements either is executed to completion or is not executed at all. Transactions make verification of JAVA CARD programs...
Verification of safety properties in the presence of transactions (2005)
Reiner Hähnle, Wojciech Mostowski
Abstract. The JAVA CARD transaction mechanism can ensure that a sequence of statements either is executed to completion or is not executed at all. Transactions make verification of JAVA CARD programs...
A theorem proving approach to analysis of secure information flow (2005)
Ádám Darvas, Reiner Hähnle, David S
Abstract. Most attempts at analysing secure information flow in programs are based on domain-specific logics. Though computationally feasible, these approaches suffer from the need for abstraction...
A theorem proving approach to analysis of secure information flow (2005)
Ádám Darvas, Reiner Hähnle, David S
Abstract. Most attempts at analysing secure information flow in programs are based on domain-specific logics. Though computationally feasible, these approaches suffer from the need for abstraction...
Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages (2005)
The purpose of this article is to clarify the role that many-valued logic can or should play in formal specification of software systems for modeling partiality. We analyse a representative set of...
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...
Symbolic model checking based on induction (2004)
Niklas Sörensson, Niklas Sörensson, Niklas Eén, Niklas Sörensson, Koen Claessen, Niklas Sörensson, ...
Applications and extensions of algorithms for SAT solving. First order theorem proving and finite model finding. SAT based Model Checking. Software Development Paradox A finite model finder for first...
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...
David A. Burke, Examiner Prof, Kristian Lindgren, Supervisor Prof, Reiner Hähnle
Improving the natural
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...
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...
Using a Software Testing Technique to Improve Theorem Proving (2004)
Reiner Hähnle, Angela Wallenburg
Most efforts to combine formal methods and software testing go in the direction of exploiting formal methods to solve testing problems, most commonly test case generation. Here we take the reverse...
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...
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...
Using a Software Testing Technique to Improve Theorem Proving (2003)
Reiner Hähnle, Angela Wallenburg
Most efforts to combine formal methods and software testing go in the direction of exploiting formal methods to solve testing problems, most commonly test case generation. Here we take the reverse...
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 Hähnle, 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...
Verification of hardware systems with first-order logic (2002)
Koen Claessen, Reiner Hähnle, Safelogic Ab
Abstract The state of the art of automatic first order logic theorem provers is advanced enough to be useful in a commercial context. This paper describes a way in which first order logic and theorem...
Verification of hardware systems with first-order logic (2002)
Koen Claessen, Reiner Hähnle, Safelogic Ab
Abstract. The state of the art of automatic first order logic theorem provers is advanced enough to be useful in a commercial context. This paper describes a way in which first order logic and...
An authoring tool for informal and formal requirements specifications (2002)
Reiner Hähnle, 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...
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...
Transformations between Signed and Classical Clause Logic (1999)
Bernhard Beckert, Reiner Hähnle, Felip Manyà
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 can be...
Transformations between signed and classical clause logic (1999)
Bernhard Beckert, Reiner Hähnle
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 can be...
Commodious Axiomatization of Quantifiers in Multiple-Valued Logic (1998)
We provide a concise axiomatization of a broad class of generalized quantifiers in many-valued logic, so- called distribution quantifiers. Although sound and complete axiomatizations for such...
Nikolaj S. Bjørner, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Peter H. Schmitt, Wolfram Menzel (karlsruhe, ...
This paper highlights a project to integrate interactive and automated theorem proving in Software Verification. Its aim is to combine the advantages of the two paradigms. We focus on one particular...
Deduction in many-valued logics: a survey. (1997)
Escalada-Imaz, Gonzalo, Hähnle, Reiner
Peer reviewed
Commodious Axiomatization of Quantifiers in Multiple-Valued Logic (1997)
. We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such...
Restart Tableaux with Selection Function (1997)
. Recently, several different sound and complete tableau calculi were introduced, all sharing the idea to use a selection function and so-called restart clauses: A-ordered tableaux, tableaux with...
Completeness for Linear Regular Negation Normal Form Inference Systems (1997)
Reiner Hähnle, Neil V. Murray, Erik Rosenthal
. Completeness proofs that generalize the Anderson-Bledsoe excess literal argument are developed for calculi other than resolution. A simple proof of the completeness of regular, connected tableaux...
Deduction in Many-Valued Logics: a Survey (1997)
Reiner Hähnle, Gonzalo Escalada-imaz
this article, there is considerable activity in MVL deduction which is why we felt justified in writing this survey. Needless to say, we cannot give a general introduction to MVL in the present...
Ordered Tableaux: Extensions and Applications (1997)
. In this paper several conceptual extensions to the theory of order-restricted free variable clausal tableaux which was initiated in [9, 8] are presented: atom orderings are replaced by the more...
Simplification of Many-Valued Formulas . . . (1997)
Bernhard Beckert, Reiner Hähnle, 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....
Simplification of Many-Valued Logic Formulas Using Anti-Links (1997)
Bernhard Beckert, Reiner Hähnle, 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....
Exploiting Data Dependencies in Many-Valued Logics (1996)
. The purpose of this paper is to make some practically relevant results in automated theorem proving available to many-valued logics with suitable modifications. We are working with a notion of...
Common Syntax of the DFG-Schwerpunktprogramm Deduktion - Version 1.2 (1996)
Reiner Hähnle, 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 a format that can easily be parsed such that it forms a...
Proving Compiler Correctness with Evolving Algebra Specifications (1996)
Bernhard Beckert, Reiner Hähnle
Introduction The purpose of this note is to define a framework for proving compiler correctness with evolving algebra (EA) specifications [2]. Although our specific domain is the verification of a...
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...
Model Generation Theorem Proving with Interval Constraints (1995)
Reiner Hähnle, Ryuzo Hasegawa, Yasuyuki Shirai
We investigate how the deduction paradigm of model generation theorem proving can be enhanced with interval- and extraval-based constraints leading to more efficient model generation in for some...
Reiner Hähnle, Stefan Klingenbeck
In resolution proof procedures refinements based on A-orderings of literals have a long tradition and are well investigated. In tableau proof procedures such refinements were only recently introduced...
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...
Efficient Deduction in Many-Valued Logics (1994)
This paper tries to identify the basic problems encountered in automated theorem proving in manyvalued logics and demonstrates to which extent they can be currently solved. To this end a number of...
Improving Temporal Logic Tableaux using Integer Constraints (1994)
Introduction In this position paper we present some ideas that aim to improve analytic tableau for temporal logics with the ultimate goal of reviving the interest in using them for temporal logic...
3TAP - The Many-Valued Theorem-Prover (1994)
Reiner Hähnle, Bernhard Beckert, Stefan Gerberding
This is the 3 T A P handbook. 3 T A P is a many-valued tableau-based theorem prover developed at the University of Karlsruhe. The handbook serves a triple purpose: first, it documents the history and...
The even more liberalized δ-rule in free variable semantic tableaux (1993)
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. In this paper we have a closer look at one of the rules of the tableau calculus presented in [3], called the δ–rule, and the modification of this rule, that has been proved to be sound...
The tableau-based theorem prover 3T A P for multiple-valued logics (1992)
Bernhard Beckert, Reiner Hähnle, Stefan Gerberding, Werner Kernig
3T A P is an acronym for 3–valued tableau–based theorem prover. It is based on the method of analytic tableaux. 3T A P has been developed at the University of Karlsruhe in cooperation with the...
An improved method for adding equality to free variable semantic tableaux (1992)
Bernhard Beckert, Reiner Hähnle
Abstract. Tableau–Based theorem provers can be extended to cover many of the nonclassical logics currently used in AI research. For both, classical and nonclassical first–order logic, equality is...