Automating inductive specification proofs

• Autorzy: Pientka B. , Kreitz Ch.
• Języki publikacji: EN

Abstrakty

EN

We present an automatic method which combines logical proof search and rippling heuristics to prove specifications. The key idea is to instantiate meta-variables in the proof with a simultaneous match based on rippling/reverse rippling heuristic. Underlying our rippling strategy is the rippling distance strategy which introduces a new powerful approach to rippling, as it avoids termination problems of other rippling strategies. Moreover, we are able to synthesize conditional substitutions for meta-variables in the proof. The strength of our approach is illustrated by discussing the specification of the integer square root and automatically synthesizing the corresponding algorithm. The described procedure has been integrated as a tactic into the NUPRL system but it can be combined with other proof methods as well.

Słowa kluczowe

EN

theorem proving; program synthesis; induction

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 1999
• Tom: Vol. 39, Nr 1,2
• Strony: 189--209
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Pientka B.

autor

Kreitz Ch.

• Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA