The following pages link to VAMPIRE (Q15455):
Displaying 50 items.
- A FOOLish encoding of the next state relations of imperative programs (Q1799102) (← links)
- MædMax: a maximal ordered completion tool (Q1799107) (← links)
- A resolution-based calculus for preferential logics (Q1799110) (← links)
- An abstraction-refinement framework for reasoning with large theories (Q1799131) (← links)
- Fast term indexing with coded context trees (Q1876097) (← links)
- The anatomy of vampire. Implementing bottom-up procedures with code trees (Q1904404) (← links)
- A navigational logic for reasoning about graph properties (Q1996850) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
- Integer induction in saturation (Q2055871) (← links)
- Neural precedence recommender (Q2055885) (← links)
- Handling transitive relations in first-order automated reasoning (Q2069868) (← links)
- Unprovability results for clause set cycles (Q2084942) (← links)
- Induction and Skolemization in saturation theorem proving (Q2084957) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- Subsumption demodulation in first-order theorem proving (Q2096454) (← links)
- Layered clause selection for theory reasoning (short paper) (Q2096461) (← links)
- Larry Wos: visions of automated reasoning (Q2102922) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- A Wos Challenge Met (Q2102924) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- An efficient subsumption test pipeline for BS(LRA) clauses (Q2104505) (← links)
- Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
- Vampire getting noisy: Will random bits help conquer chaos? (system description) (Q2104552) (← links)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) (← links)
- Inductive benchmarks for automated reasoning (Q2128807) (← links)
- Automated generation of exam sheets for automated deduction (Q2128822) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
- Eliminating models during model elimination (Q2142079) (← links)
- Learning theorem proving components (Q2142080) (← links)
- Symmetry avoidance in MACE-style finite model finding (Q2180212) (← links)
- A neurally-guided, parallel theorem prover (Q2180215) (← links)
- Herbrand constructivization for automated intuitionistic theorem proving (Q2180528) (← links)
- Introducing \(H\), an institution-based formal specification and verification language (Q2183716) (← links)
- Relaxed weighted path order in theorem proving (Q2209265) (← links)
- Induction with generalization in superposition reasoning (Q2219385) (← links)
- Making theory reasoning simpler (Q2233504) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Inspection and selection of representations (Q2287916) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments (Q2303247) (← links)
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) (← links)
