VAMPIRE

swMATH2918MaRDI QIDQ15455FDOQ15455

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Blocking and other enhancements for bottom-up model generation methods
• Restricted combinatory unification
• A posthumous contribution by Larry Wos: excerpts from an unpublished column
• A Wos Challenge Met
• Larry Wos: visions of automated reasoning
• Set of support, demodulation, paramodulation: a historical perspective
• Verifying Whiley programs with Boogie
• An efficient subsumption test pipeline for BS(LRA) clauses
• Vampire getting noisy: Will random bits help conquer chaos? (system description)
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• AC simplifications and closure redundancies in the superposition calculus
• A neurally-guided, parallel theorem prover
• An interactive derivation viewer
• Automated theorem proving in quasigroup and loop theory
• A navigational logic for reasoning about graph properties
• Fast term indexing with coded context trees
• Efficient instance retrieval with standard and relational path indexing
• Document models
• Extensional higher-order paramodulation in Leo-III
• TPTP, TSTP, CASC, etc.
• Verifying Tight Logic Programs with anthem and vampire
• Title not available (Why is that?)
• Towards satisfiability modulo parametric bit-vectors
• Portfolio theorem proving and prover runtime prediction for geometry
• Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
• A comprehensive framework for saturation theorem proving
• Superposition with lambdas
• Selecting the selection
• Internal guidance for Satallax
• Encoding First Order Proofs in SAT
• Machine learning guidance for connection tableaux
• Towards a unified ordering for superposition-based automated reasoning
• A verified SAT solver framework with learn, forget, restart, and incrementality
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Smart matching
• Encoding monomorphic and polymorphic types
• System description: E.T. 0.1
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
• Inductive benchmarks for automated reasoning
• Implementing Superposition in iProver (System Description)
• Neural precedence recommender
• Title not available (Why is that?)
• A generic framework for implicate generation modulo theories
• A FOOLish encoding of the next state relations of imperative programs
• An abstraction-refinement framework for reasoning with large theories
• Superposition for \(\lambda\)-free higher-order logic
• Superposition with datatypes and codatatypes
• Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
• Unifying theories of programming in Isabelle
• From search to computation: redundancy criteria and simplification at work
• Making theory reasoning simpler
• From LCF to Isabelle/HOL
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Induction in saturation-based proof search
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Verifying strong equivalence of programs in the input language of \textsc{gringo}
• Restricting backtracking in connection calculi
• Handling transitive relations in first-order automated reasoning
• Superposition with equivalence reasoning and delayed clause normal form transformation
• Formal mathematics on display: a wiki for Flyspeck
• Gibbard's collapse theorem for the indicative conditional: an axiomatic approach
• On combining algebraic specifications with first-order logic via Athena
• Property-directed inference of universal invariants or proving their absence
• Symmetry avoidance in MACE-style finite model finding
• Induction and Skolemization in saturation theorem proving
• Computing Parameterized Invariants of Parameterized Petri Nets
• Combining induction and saturation-based theorem proving
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Herbrand constructivization for automated intuitionistic theorem proving
• Extending Sledgehammer with SMT solvers
• GKC: a reasoning system for large knowledge bases
• JGXYZ: an ATP system for gap and glut logics
• Automated search for impossibility theorems in social choice theory: ranking sets of objects
• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
• Mechanising first-order temporal resolution
• AVATAR: The Architecture for First-Order Theorem Provers
• A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
• Automatic construction and verification of isotopy invariants
• The Relative Power of Semantics and Unification
• Lemma Mining over HOL Light
• Automated Reasoning
• Title not available (Why is that?)
• Title not available (Why is that?)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Interpolation and Symbol Elimination
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Decidable Fragments of Many-Sorted Logic
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• MaLeS: a framework for automatic tuning of automated theorem provers
• The higher-order prover \textsc{Leo}-II
• Semantically-guided goal-sensitive reasoning: model representation
• Semi-intelligible Isar proofs from machine-generated proofs
• Practical solution techniques for first-order MDPs
• Mathematical Knowledge Management
• System for Automated Deduction (SAD): A Tool for Proof Verification
• Automated Deduction – CADE-20
• Mining the Archive of Formal Proofs
• Practical algorithms for unsatisfiability proof and core generation in SAT solvers

This page was built for software: VAMPIRE