AVATAR
From MaRDI portal
Cited in
(78)- FRAT
- OTTER
- VAMPIRE
- SPASS
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Superposition with structural induction
- Zeno
- HipSpec
- Towards satisfiability modulo parametric bit-vectors
- A unifying splitting framework
- Integer induction in saturation
- Superposition with first-class booleans and inprocessing clausification
- StarExec
- Unprovability results for clause set cycles
- Induction and Skolemization in saturation theorem proving
- Subsumption demodulation in first-order theorem proving
- Layered clause selection for theory reasoning (short paper)
- Theorem proving as constraint solving with coherent logic
- Vampire getting noisy: Will random bits help conquer chaos? (system description)
- Eliminating models during model elimination
- CVC4
- iProver
- Equinox
- Herbrand constructivization for automated intuitionistic theorem proving
- Combining induction and saturation-based theorem proving
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Combining proverif and automated theorem provers for security protocol verification
- Induction in saturation-based proof search
- Hipster
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Locales
- Easychair
- Beagle
- randoCoP
- URSA
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Selecting the selection
- AVATAR: The Architecture for First-Order Theorem Provers
- Cyclist
- IsaFoL
- InKa
- DISCOUNT
- Saturate
- A learning-based fact selector for Isabelle/HOL
- ProofTool
- Scavenger
- DPT
- Superposition Calculus
- MadMax
- Twee
- Logtk
- SAT Solver Verification
- Jinja not Java
- Nested Multisets
- FLOTTER
- Zipperposition
- SMTCoq
- GKC
- WhaleProver
- Slakje
- GNU parallel
- Imandra
- Ordered_Resolution_Prover
- Saturation_Framework
- SPASS-AR
- SAT-Inspired Eliminations for Superposition
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
- Robinson arithmetic
- BanditFuzz
- EUCLID
- qbf2epr
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Vampire with a brain is a good ITP hammer
- Quantifier simplification by unification in SMT
This page was built for software: AVATAR
