AVATAR
AVATAR: The Architecture for First-Order Theorem Provers. This paper describes a new architecture for first-order resolution and superposition theorem provers called AVATAR (Advanced Vampire Architecture for Theories and Resolution). Its original motivation comes from a problem well-studied in the past — dealing with problems having clauses containing propositional variables and other clauses that can be split into components with disjoint sets of variables. Such clauses are common for problems coming from applications, for example in program verification and program analysis, where many ground literals occur in the problems and even more are generated during the proof-search. ..
Keywords for this software
References in zbMATH (referenced in 16 articles )
Showing results 1 to 16 of 16.
Sorted by year (- Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
- Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei: Induction with generalization in superposition reasoning (2020)
- Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
- Teucke, Andreas; Weidenbach, Christoph: SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (2020)
- Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
- Li, Di Long; Tiu, Alwen: Combining proverif and automated theorem provers for security protocol verification (2019)
- Reger, Giles; Voronkov, Andrei: Induction in saturation-based proof search (2019)
- Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
- Reger, Giles; Suda, Martin; Voronkov, Andrei: Unification with abstraction and theory instantiation in saturation-based reasoning (2018)
- Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2018)
- Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
- Cruanes, Simon: Superposition with structural induction (2017)
- Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei: Selecting the selection (2016)
- Voronkov, Andrei: AVATAR: The architecture for first-order theorem provers (2014) ioport