English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Implementation of a prover
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-03-12 (21:41)
From: David Baelde <david.baelde@g...>
Subject: Implementation of a prover
Hi list,

There are well-known implementation techniques for depth-first theorem
proving, using continuation-passing style (success/failure
continuations). But these techniques do not easily allow the building
of a proof witness. This is nice when you have a working proof-search
procedure but not when you're still playing with a logic, trying to
find the right procedure or more generally when you just want an
interactive prover.

I've started to look for a way to define rules as tactics in such a
way that these core functions can be used with or without a proof
witness construction procedure. I've had enough for today and I wanted
to know if anyone done that or knows a link to anything like that.

Any idea?