AVATAR: The Architecture for First-Order Theorem Provers
From MaRDI portal
Publication:2920991
DOI10.1007/978-3-319-08867-9_46zbMath1495.68240OpenAlexW2221495694MaRDI QIDQ2920991
Publication date: 29 September 2014
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-08867-9_46
Related Items (36)
Vampire with a brain is a good ITP hammer ⋮ Quantifier simplification by unification in SMT ⋮ Eliminating models during model elimination ⋮ Cooperating Proof Attempts ⋮ System Description: E.T. 0.1 ⋮ A learning-based fact selector for Isabelle/HOL ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Unifying splitting ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Making higher-order superposition work ⋮ 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 ⋮ Non-clausal redundancy properties ⋮ A unifying splitting framework ⋮ Integer induction in saturation ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Neural precedence recommender ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Induction in saturation-based proof search ⋮ 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
Uses Software
This page was built for publication: AVATAR: The Architecture for First-Order Theorem Provers
