AVATAR: The Architecture for First-Order Theorem Provers
From MaRDI portal
Recommendations
- First-order theorem proving: foreword
- Theorem Proving in Higher Order Logics
- First-order logic theorem proving and model building via approximation and instantiation
- scientific article; zbMATH DE number 1300967
- scientific article; zbMATH DE number 46359
- Implementing and evaluating provers for first-order modal logics
- Satallax: An Automatic Higher-Order Prover
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
Cited in
(55)- 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
- Towards satisfiability modulo parametric bit-vectors
- Improving ENIGMA-style clause selection while learning from history
- Layered clause selection for theory reasoning (short paper)
- Selecting the selection
- A comprehensive framework for saturation theorem proving
- Making higher-order superposition work
- Certifying incremental SAT solving
- How much should this symbol weigh? A GNN-advised clause selection
- Eliminating models during model elimination
- Learning guided automated reasoning: a brief survey
- Lemma discovery and strategies for automated induction
- Reducibility constraints in superposition
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- 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
- Unifying splitting
- A learning-based fact selector for Isabelle/HOL
- System description: E.T. 0.1
- The 481 ways to split a clause and deal with propositional variables
- Finding connections via satisfiability solving
- Non-clausal redundancy properties
- Neural precedence recommender
- Superposition with first-class booleans and inprocessing clausification
- Making higher-order superposition work
- Playing with AVATAR
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- Efficient neural clause-selection reinforcement
- Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories
- Towards bit-width-independent proofs in SMT solvers
- Induction in saturation-based proof search
- A comprehensive framework for saturation theorem proving
- Program Synthesis in Saturation
- SAT-Based Subsumption Resolution
- Superposition with Delayed Unification
- Invariant neural architecture for learning term synthesis in instantiation proving
- Cooperating proof attempts
- Unprovability results for clause set cycles
- Theorem proving as constraint solving for coherent logic with function symbols
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Theorem proving as constraint solving with coherent logic
- Integer induction in saturation
- SAT solving for variants of first-order subsumption
- 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
- ALASCA: reasoning in quantified linear arithmetic
- Automating induction by reflection
- Combining induction and saturation-based theorem proving
This page was built for publication: AVATAR: The Architecture for First-Order Theorem Provers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2920991)
