Version française
Home     About     Download     Resources     Contact us    
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: -- (:)
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?
-- 
David