Pages that link to "Item:Q2920991"

The following pages link to AVATAR: The Architecture for First-Order Theorem Provers (Q2920991):

Displaying 39 items.

• A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
• Vampire with a brain is a good ITP hammer (Q831938) (← links)
• Quantifier simplification by unification in SMT (Q831945) (← links)
• A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
• Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
• Non-clausal redundancy properties (Q2055860) (← links)
• A unifying splitting framework (Q2055869) (← links)
• Integer induction in saturation (Q2055871) (← links)
• Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
• Neural precedence recommender (Q2055885) (← links)
• Improving ENIGMA-style clause selection while learning from history (Q2055886) (← links)
• Unprovability results for clause set cycles (Q2084942) (← links)
• Induction and Skolemization in saturation theorem proving (Q2084957) (← links)
• Subsumption demodulation in first-order theorem proving (Q2096454) (← links)
• Layered clause selection for theory reasoning (short paper) (Q2096461) (← links)
• Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
• Vampire getting noisy: Will random bits help conquer chaos? (system description) (Q2104552) (← links)
• Eliminating models during model elimination (Q2142079) (← links)
• Combining induction and saturation-based theorem proving (Q2303240) (← links)
• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) (← links)
• Combining proverif and automated theorem provers for security protocol verification (Q2305427) (← links)
• Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
• Induction in saturation-based proof search (Q2305434) (← links)
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
• Selecting the Selection (Q2817931) (← links)
• Cooperating Proof Attempts (Q3454105) (← links)
• System Description: E.T. 0.1 (Q3454109) (← links)
• SAT-Inspired Eliminations for Superposition (Q5875949) (← links)
• Making higher-order superposition work (Q5918403) (← links)
• A comprehensive framework for saturation theorem proving (Q5918558) (← links)
• Making higher-order superposition work (Q5918575) (← links)
• Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5919011) (← links)
• A comprehensive framework for saturation theorem proving (Q5970776) (← links)
• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule (Q6086313) (← links)
• Unifying splitting (Q6103590) (← links)
• ALASCA: reasoning in quantified linear arithmetic (Q6535381) (← links)
• Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version) (Q6610379) (← links)
• Invariant neural architecture for learning term synthesis in instantiation proving (Q6650564) (← links)