AVATAR
From MaRDI portal
Software:40350
No author found.
Related Items (33)
Vampire with a brain is a good ITP hammer ⋮ Quantifier simplification by unification in SMT ⋮ Eliminating models during model elimination ⋮ A learning-based fact selector for Isabelle/HOL ⋮ AVATAR: The Architecture for First-Order Theorem Provers ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Herbrand constructivization for automated intuitionistic theorem proving ⋮ Superposition with structural induction ⋮ Induction with generalization in superposition reasoning ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Making higher-order superposition work ⋮ A comprehensive framework for saturation theorem proving ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Combining induction and saturation-based theorem proving ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Selecting the Selection ⋮ A unifying splitting framework ⋮ Integer induction in saturation ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Induction in saturation-based proof search ⋮ Unification with abstraction and theory instantiation in saturation-based reasoning ⋮ 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) ⋮ A comprehensive framework for saturation theorem proving ⋮ Theorem proving as constraint solving with coherent logic ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description) ⋮ SAT-Inspired Eliminations for Superposition
This page was built for software: AVATAR
