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)
- Herbrand constructivization for automated intuitionistic theorem proving
- GKC: a reasoning system for large knowledge bases
- JGXYZ: an ATP system for gap and glut logics
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Title not available (Why is that?)
- Equinox
- ileanCoP
- ForTheL
- DLog
- leanCoP
- InvGen
- KAON2
- SmallCheck
- SAD
- Racer
- JProver
- mkbTT
- PARTHEO
- Gandalf
- E Theorem Prover
- Slothrop
- Flyspeck
- Ivy
- PRocH
- MaLARea
- MathWeb
- NMRDPP
- TeMP
- SystemOnTPTP
- Hipster
- HOLyHammer
- Cool
- Mcmt
- Jahob
- YAGO
- Locales
- Spartacus
- Easychair
- HOT
- Beagle
- Lingva
- Cubicle
- Saucy
- DynaMate
- FOOL
- CLPGUI
- E-MaLeS
- TRP++
- randoCoP
- SigmaKEE
- ArgoTriCS
- EQP
- URSA
- SInE
- BliStr
- HyLoRes
- MSPASS
- TRAMP
- Cyclist
- AGORA
- BliStrTune
- Leo-III
- aspcud
- IsaFoL
- CLAM
- CLIN
- DISCOUNT
- Openproof
- InKa
- Leo
- Lambda-Clam
- LOUI
- Omega-ANTS
- Oyster
- SNARK
- Speedith
- Spacer
- Waldmeister
- Shred
- RADA
- FEMaLeCoP
- Bliksem
- Doris
- Angelic Verification
- E-KRHyper
- IDV
- KOMET
- Medmaker
- P.rex
- PROTEIN
- UCPOP
- Saturate
- SWI-Prolog
- SRASS
- SAD as a mathematical assistant -- how should we go from here to there?
- MædMax: a maximal ordered completion tool
- Hammer for Coq: automation for dependent type theory
- Lingva: generating and proving program properties using symbol elimination
- ProofWatch: watchlist guidance for large theories in E
This page was built for software: VAMPIRE
