[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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? -- David