sneeuwballen/zipperposition

fast proof checker

c-cube opened this issue 5 years ago · 0 comments

c-cube commented 5 years ago

possible investigation leads:

use a SMT instead of tableau architecture (sidekick?)
imperative CC
use external prover (vendored?)