The following pages link to VAMPIRE (Q15455):
Displaying 50 items.
- Restricted combinatory unification (Q2305407) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Combining proverif and automated theorem provers for security protocol verification (Q2305427) (← links)
- On invariant synthesis for parametric systems (Q2305429) (← links)
- Induction in saturation-based proof search (Q2305434) (← links)
- JGXYZ: an ATP system for gap and glut logics (Q2305437) (← links)
- GKC: a reasoning system for large knowledge bases (Q2305438) (← links)
- Unification with abstraction and theory instantiation in saturation-based reasoning (Q2324203) (← links)
- Verifying strong equivalence of programs in the input language of \textsc{gringo} (Q2326735) (← links)
- Set-blocked clause and extended set-blocked clause in first-order logic (Q2333858) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- On interpolation in automated theorem proving (Q2352502) (← links)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
- Using relation-algebraic means and tool support for investigating and computing bipartitions (Q2360655) (← links)
- ENIGMA: efficient learning-based inference guiding machine (Q2364687) (← links)
- Alternating two-way AC-tree automata (Q2373699) (← links)
- The model evolution calculus as a first-order DPLL method (Q2389629) (← links)
- Splitting proofs for interpolation (Q2405256) (← links)
- Detecting inconsistencies in large first-order knowledge bases (Q2405258) (← links)
- Resolution with order and selection for hybrid logics (Q2429982) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically (Q2484410) (← links)
- Superposition with equivalence reasoning and delayed clause normal form transformation (Q2486577) (← links)
- Mechanising first-order temporal resolution (Q2486579) (← links)
- Efficient instance retrieval with standard and relational path indexing (Q2486586) (← links)
- A new Gödelian argument for hypercomputing minds based on the busy beaver problem (Q2495984) (← links)
- From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
- Portfolio theorem proving and prover runtime prediction for geometry (Q2631959) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Theorem proving using clausal resolution: from past to present (Q2695485) (← links)
- (Q2723432) (← links)
- Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories (Q2740996) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Selecting the Selection (Q2817931) (← links)
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (Q2817933) (← links)
- Internal Guidance for Satallax (Q2817934) (← links)
- : A Resolution-Based Prover for Multimodal K (Q2817940) (← links)
- Finding Finite Models in Multi-sorted First-Order Logic (Q2818025) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- Formal Mathematics on Display: A Wiki for Flyspeck (Q2843012) (← links)
- Detection of First Order Axiomatic Theories (Q2849492) (← links)
- Presenting and explaining Mizar (Q2867936) (← links)
- An interactive derivation viewer (Q2867942) (← links)
- Tree Interpolation in Vampire (Q2870125) (← links)
- Lemma Mining over HOL Light (Q2870150) (← links)
