The following pages link to VAMPIRE (Q15455):
Displaying 50 items.
- Fingerprint Indexing for Paramodulation and Rewriting (Q2908518) (← links)
- AVATAR: The Architecture for First-Order Theorem Provers (Q2920991) (← links)
- Playing in the grey area of proofs (Q2942878) (← links)
- Unifying Theories of Programming in Isabelle (Q2948230) (← links)
- Random Forests for Premise Selection (Q2964471) (← links)
- Lemmatization for Stronger Reasoning in Large Theories (Q2964472) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules (Q2987065) (← links)
- An Introduction to Practical Formal Methods Using Temporal Logic (Q2996923) (← links)
- (Q3006508) (← links)
- MaLeCoP Machine Learning Connection Prover (Q3010374) (← links)
- (Q3075241) (← links)
- Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects (Q3081450) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Expressing Polymorphic Types in a Many-Sorted Language (Q3172884) (← links)
- Translating a Dependently-Typed Logic to First-Order Logic (Q3184740) (← links)
- Simulation and Synthesis of Deduction Calculi (Q3185770) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) (← links)
- Cooperating Proof Attempts (Q3454105) (← links)
- System Description: E.T. 0.1 (Q3454109) (← links)
- Playing with AVATAR (Q3454110) (← links)
- Lingva: Generating and Proving Program Properties Using Symbol Elimination (Q3455056) (← links)
- Efficient Low-Level Connection Tableaux (Q3455764) (← links)
- Ordered Resolution for Coalition Logic (Q3455769) (← links)
- Extensional Crisis and Proving Identity (Q3457789) (← links)
- Reasoning About Loops Using Vampire in KeY (Q3460073) (← links)
- Decidable Fragments of Many-Sorted Logic (Q3498453) (← links)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties (Q3498479) (← links)
- ATP Cross-Verification of the Mizar MPTP Challenge Problems (Q3498492) (← links)
- TPTP, TSTP, CASC, etc. (Q3499763) (← links)
- (Q3509041) (← links)
- Source-Level Proof Reconstruction for Interactive Theorem Proving (Q3523178) (← links)
- Automated Reasoning About Metric and Topology (Q3533154) (← links)
- SMELS: Satisfiability Modulo Equality with Lazy Superposition (Q3540073) (← links)
- Resolution-Like Theorem Proving for High-Level Conditions (Q3540406) (← links)
- Development of Correct Graph Transformation Systems (Q3540429) (← links)
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (Q3541699) (← links)
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) (Q3541709) (← links)
- Proof Systems for Effectively Propositional Logic (Q3541721) (← links)
- Implementing a fair monodic temporal logic prover (Q3568221) (← links)
- Large theory reasoning with SUMO at CASC (Q3568226) (← links)
- Practical algorithms for unsatisfiability proof and core generation in SAT solvers (Q3568227) (← links)
- Restricting backtracking in connection calculi (Q3568228) (← links)
- An application of automated reasoning in natural language question answering (Q3568232) (← links)
- Automated theorem proving in quasigroup and loop theory (Q3568233) (← links)
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools. (Q3568690) (← links)
- Smart Matching (Q3582713) (← links)
- Handling Polymorphism in Automated Deduction (Q3608778) (← links)
- Labelled Clauses (Q3608781) (← links)
