Theory Development in an Automated Theorem Prover

  • Stéphane Ricour

Student thesis: Master typesMaster in Computer science

Abstract

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.
Date of Award1991
Original languageEnglish
Awarding Institution
  • University of Namur
SupervisorBaudouin LE CHARLIER (Supervisor)

Cite this

'