The following pages link to VAMPIRE (Q15455):
Displaying 50 items.
- System for Automated Deduction (SAD): A Tool for Proof Verification (Q3608785) (← links)
- Encoding First Order Proofs in SAT (Q3608794) (← links)
- Combining Type Theory and Untyped Set Theory (Q3613410) (← links)
- First-Order Logic with Dependent Types (Q3613421) (← links)
- Implementing Temporal Logics: Tools for Execution and Proof (Q3623967) (← links)
- Combinations of Theories for Decidable Fragments of First-Order Logic (Q3655205) (← links)
- Invariant and Type Inference for Matrices (Q3656882) (← links)
- Automated Reasoning (Q3723724) (← links)
- Efficient access mechanisms for tabled logic programs (Q4223452) (← links)
- (Q4409888) (← links)
- (Q4415137) (← links)
- (Q4447245) (← links)
- (Q4536327) (← links)
- (Q4539595) (← links)
- (Q4539610) (← links)
- (Q4539622) (← links)
- Simple and Efficient Clause Subsumption with Feature Vector Indexing (Q4913860) (← links)
- Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach (Q4913867) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
- Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto (Q4913999) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- From Search to Computation: Redundancy Criteria and Simplification at Work (Q4916077) (← links)
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning (Q4916080) (← links)
- The Relative Power of Semantics and Unification (Q4916085) (← links)
- One Logic to Use Them All (Q4928425) (← links)
- E-MaLeS 1.1 (Q4928455) (← links)
- (Q4989394) (← links)
- (Q5020535) (← links)
- (Q5020994) (← links)
- (Q5028439) (← links)
- (Q5028442) (← links)
- A First-Order Logic with Frames (Q5041109) (← links)
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (Q5043584) (← links)
- Computing Parameterized Invariants of Parameterized Petri Nets (Q5044400) (← links)
- Teaching Automated Theorem Proving by Example: PyRes 1.2 (Q5048999) (← links)
- A Polymorphic Vampire (Q5049013) (← links)
- Implementing Superposition in iProver (System Description) (Q5049017) (← links)
- Make E Smart Again (Short Paper) (Q5049019) (← links)
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) (Q5049022) (← links)
- A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description) (Q5049030) (← links)
- Prolog Technology Reinforcement Learning Prover (Q5049033) (← links)
- Towards Verifying Logic Programs in the Input Language of clingo (Q5049051) (← links)
- The CADE-28 Automated Theorem Proving System Competition – CASC-28 (Q5069650) (← links)
- Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Q5086225) (← links)
- Verifying Tight Logic Programs with anthem and vampire (Q5140011) (← links)
- An Interactive Driver for Goal-directed Proof Strategies (Q5166499) (← links)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic (Q5191100) (← links)
- Interpolation and Symbol Elimination (Q5191103) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Experimenting with Deduction Modulo (Q5200022) (← links)
