Oyster/Clam is an automated theorem prover based on Martin-Löf's constructive theory of types. Recent work has centred round the notion of proof plan to guide the search for proofs. Experiments with proof plans for finding proofs by induction, using heuristics adapted from the work of Boyer and Moore, have shown encouraging results. This work apply this approach to the data structure of finite sets. A systematic approach is taken to building up the machinery needed to use such a theory, in the form of suitable tactics and a library of theorem.
| la date de réponse | 1991 |
|---|
| langue originale | Anglais |
|---|
| L'institution diplômante | |
|---|
| Superviseur | Baudouin LE CHARLIER (Promoteur) |
|---|
Theory Development in an Automated Theorem Prover
Ricour, S. (Auteur). 1991
Student thesis: Master types › Master en sciences informatiques