Skip to content

Vampire Subprocess Prover

Pre-release
Pre-release
Compare
Choose a tag to compare
@James-Oswald James-Oswald released this 09 May 04:56
v0.0.1
141dc78

This pre-release integrates our fast tree formulae representation with a vampire subprocess prover that can determine if a first order formula is a theorem.

  • Support for formulae representation up to 2nd order. Some utilities for checking formula and term properties.
  • A first order TPTP converter for formulae.
  • A Problem class for representing theorem proving problems.
  • A Vampire Subprocess prover which will attempt to solve a given problem by calling vampire on it.
Assets 2
Loading