PV6 ⊧ Vampirecan produce proofs for theorems in first order logic

First-order theorem prover

Application domain/field

• Theorem proving
• First-order logic

Type of tool

Automatic theorem prover

Expected input

• First-order logic theorem
• Optional: Memory-limit and/or time-limit

Format:

• First-order logic theorem: TPTP syntax (.tptp file)
• Memory/time-limit: parameter when calling Vampire

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