VAMPIRE
From MaRDI portal
Software:15455
swMATH2918MaRDI QIDQ15455FDOQ15455
Author name not available (Why is that?)
Official website: https://vprover.github.io/history.html
Source code repository: https://github.com/vprover/vampire
Cited In (only showing first 100 items - show all)
- Extending Sledgehammer with SMT solvers
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- D-Finder
- GCLC
- ILTP
- LEO-II
- ML
- TPS
- MPTP 0.2
- SMT-LIB
- SPASS
- Isar
- Gringo
- MoMM
- Mizar
- Yices
- cvc3
- LPL software
- SPASS+T
- STRIP
- Proof General
- UCLID
- Prover9
- SIMPLIFY
- z3
- HOL
- FINDER
- HOL Light
- DCTP
- MUltlog
- SATCHMO
- SCOTT
- E-Darvin
- TSPASS
- MUSCADET
- Satallax
- Mace4
- AURA
- NiVER
- MML
- Zenon
- Kodkod
- Zap
- E-SETHEO
- Sledgehammer
- ArgoCLP
- PicoSAT
- ML4PG
- ESC4
- gcl
- MaLeCoP
- OpenGeoProver
- veriT
- NQTHM
- TATL
- CVC Lite
- FluCaP
- HipSpec
- KRATOS
- MaSh
- Augur 2
- Zeno
- MBase
- WinGCLC
- Leon
- CERES
- StarExec
- CheckVML
- CVC4
- iProver-Eq
- Equinox
- iProver
- JAMPACK
- ileanCoP
- ForTheL
- DLog
- leanCoP
- InvGen
- KAON2
- SmallCheck
- SAD
- Racer
- JProver
- TLAPS
- mkbTT
- PARTHEO
- Gandalf
- E Theorem Prover
- Slothrop
- Flyspeck
- WhyML
- PRocH
- TeMP
- MizAR 40 for Mizar 40
- Model evolution with equality -- revised and implemented
- MPTP 0.2: Design, implementation, and initial experiments
- MaLeCoP. Machine learning connection prover
- Automatic proof and disproof in Isabelle/HOL
- Metis
- Relaxed weighted path order in theorem proving
This page was built for software: VAMPIRE
