VAMPIRE
From MaRDI portal
VAMPIRE Q15455
Cited in
(only showing first 100 items - show all)- Lightweight relevance filtering for machine-generated resolution problems
- Solving the \$100 modal logic challenge
- Automated verification of refinement laws
- Solving quantified verification conditions using satisfiability modulo theories
- A new methodology for developing deduction methods
- Aligator
- Dafny
- D-Finder
- GCLC
- ILTP
- LEO-II
- MiniSat
- PyRes
- Nitpick
- SETHEO
- OCL2AC
- lazyCoP
- Goeland
- SMAC3
- FRAT
- RegStab
- TPS
- ML
- Hilberticus
- Stratified resolution
- Limited resource strategy in resolution theorem proving
- OilEd
- Isabelle/HOL
- AutoBayes/CC
- LWB
- BarcelogicTools
- MPTP
- MPTP 0.2
- IMPACT
- OTTER
- THF0
- PVS
- Paradox
- Evaluating general purpose automated theorem proving systems
- SMT-LIB
- SPASS
- TPTP
- Darwin
- Yices
- Metis
- Towards a unified ordering for superposition-based automated reasoning
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Hammer for Coq: automation for dependent type theory
- Isar
- SPASS+T
- Gringo
- STRIP
- MoMM
- UCLID
- Mizar
- Superposition with structural induction
- On combining algebraic specifications with first-order logic via Athena
- LPL software
- Property-directed inference of universal invariants or proving their absence
- cvc3
- z3
- Proof General
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Document models
- Prover9
- SIMPLIFY
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- HOL
- ProofWatch: watchlist guidance for large theories in E
- Superposition for -free higher-order logic
- A generic framework for implicate generation modulo theories
- Superposition with datatypes and codatatypes
- A FOOLish encoding of the next state relations of imperative programs
- MædMax: a maximal ordered completion tool
- A resolution-based calculus for preferential logics
- An abstraction-refinement framework for reasoning with large theories
- FINDER
- TSPASS
- HOL Light
- MUltlog
- SATCHMO
- DCTP
- Fast term indexing with coded context trees
- SCOTT
- Zenon
- Zap
- Satallax
- E-Darvin
- MUSCADET
- Mace4
- NiVER
- MML
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- AURA
- Sledgehammer
- Kodkod
- PicoSAT
- ML4PG
- E-SETHEO
- OpenGeoProver
This page was built for software: VAMPIRE
