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