Author name cluster

Helko Lehmann

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

LOPSTR Conference 2003 Invited Paper

Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce

Helko Lehmann
Michael Leuschel

Abstract In this paper we discuss the similarities between program specialisation and inductive theorem proving, and then show how program specialisation can be used to perform inductive theorem proving. We then study this relationship in more detail for a particular class of problems (verifying infinite state Petri nets) in order to establish a clear link between program specialisation and inductive theorem proving. In particular, we use the program specialiser ecce to generate specifications, hypotheses and proof scripts in the theory format of the proof assistant Isabelle. Then, in many cases, Isabelle can automatically execute these proof scripts and thereby verify the soundness of ecce ’s verification process and of the correspondence between program specialisation and inductive theorem proving.

Details

LPAR Conference 2000 Conference Paper

Solving Planning Problems by Partial Deduction

Helko Lehmann
Michael Leuschel

Abstract We develop an abstract partial deduction method capable of solving planning problems in the Fluent Calculus. To this end, we extend “classical” partial deduction to accommodate both, equational theories and regular type information. We show that our new method is actually complete for conjunctive planning problems in the propositional Fluent Calculus. Furthermore, we believe that our approach can also be used for more complex systems, e. g. , in cases where completeness can not be guaranteed due to general undecidability.

Details