The following pages link to VAMPIRE (Q15455):
Displaying 50 items.
- MaLeS: a framework for automatic tuning of automated theorem provers (Q286787) (← links)
- MizAR 40 for Mizar 40 (Q286800) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Multi-completion with termination tools (Q352956) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Fast and slow enigmas and parental guidance (Q831937) (← links)
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- Quantifier simplification by unification in SMT (Q831945) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Practical solution techniques for first-order MDPs (Q835833) (← links)
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (Q841684) (← links)
- First-order temporal verification in practice (Q851137) (← links)
- Simplifying proofs in Fitch-style natural deduction systems (Q851139) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- Things to know when implementing KBO (Q861708) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- MPTP 0.2: Design, implementation, and initial experiments (Q877826) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Automatic construction and verification of isotopy invariants (Q928664) (← links)
- Combined reasoning by automated cooperation (Q946572) (← links)
- The logicist manifesto: At long last let logic-based artificial intelligence become a field unto itself (Q959049) (← links)
- Resolution is cut-free (Q972424) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Solving the \$100 modal logic challenge (Q1006738) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- Stratified resolution (Q1404977) (← links)
- Limited resource strategy in resolution theorem proving (Q1404979) (← links)
- Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
- Towards a unified ordering for superposition-based automated reasoning (Q1662244) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Superposition with structural induction (Q1687553) (← links)
- On combining algebraic specifications with first-order logic via Athena (Q1697091) (← links)
- Property-directed inference of universal invariants or proving their absence (Q1702932) (← links)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)
- Document models (Q1709112) (← links)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (Q1735326) (← links)
- ProofWatch: watchlist guidance for large theories in E (Q1791167) (← links)
- Superposition for \(\lambda\)-free higher-order logic (Q1799065) (← links)
- A generic framework for implicate generation modulo theories (Q1799090) (← links)
- Superposition with datatypes and codatatypes (Q1799098) (← links)
