AVATAR

swMATH28636MaRDI QIDQ40350FDOQ40350

Author name not available (Why is that?)

Cited In (33)

• 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)
• Eliminating models during model elimination
• Subsumption demodulation in first-order theorem proving
• A verified SAT solver framework with learn, forget, restart, and incrementality
• A learning-based fact selector for Isabelle/HOL
• Selecting the Selection
• Superposition with first-class booleans and inprocessing clausification
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• Induction with generalization in superposition reasoning
• 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
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
• Theorem proving as constraint solving with coherent logic
• Integer induction in saturation
• Combining proverif and automated theorem provers for security protocol verification
• SAT-Inspired Eliminations for Superposition
• 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