PV6 Vampirecan produce proofs for theorems in first order logic

First-order theorem prover

Application domain/field

Type of tool

Automatic theorem prover

Expected input

Format:

Expected output

Reason for termination (refutation was found, time/memory limit was reached, satisfiability detected, ...) It also prints some statistics about the proof attempt.

Internals

Vampire uses proof by refutation to try and determine whether a conjecture is correct. If Vampire finds a refutation, then it will show the inference steps that were taken, i.e. it'll show a proof. Uses MiniSat, Z3.

Comments

License: BSD 3-Clause license

Links

Related papers

Last publication date

2017

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.