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
• Formal Mathematics on Display: A Wiki for Flyspeck
• 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?)
• Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto
• 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
• From Search to Computation: Redundancy Criteria and Simplification at Work
• A comprehensive framework for saturation theorem proving
• Superposition with lambdas
• Encoding First Order Proofs in SAT
• Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach
• 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
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• Internal Guidance for Satallax
• Selecting the Selection
• Inductive benchmarks for automated reasoning
• 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
• Induction with generalization in superposition reasoning
• 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
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
• : A Resolution-Based Prover for Multimodal K
• On combining algebraic specifications with first-order logic via Athena
• Encoding Monomorphic and Polymorphic Types
• Property-directed inference of universal invariants or proving their absence
• Symmetry avoidance in MACE-style finite model finding
• Unifying Theories of Programming in Isabelle
• Induction and Skolemization in saturation theorem proving
• System Description: E.T. 0.1
• Computing Parameterized Invariants of Parameterized Petri Nets
• Smart Matching
• 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
• GKC: a reasoning system for large knowledge bases
• JGXYZ: an ATP system for gap and glut logics
• 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
• MaLeCoP Machine Learning Connection Prover
• Title not available (Why is that?)
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• The Relative Power of Semantics and Unification
• Automatic Proof and Disproof in Isabelle/HOL
• 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
• Sine Qua Non for Large Theory Reasoning
• 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
• Lingva: Generating and Proving Program Properties Using Symbol Elimination
• 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

This page was built for software: VAMPIRE