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
• 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
• Smart matching
• 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
• Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
• Induction with generalization in superposition reasoning
• 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
• 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
• Combining induction and saturation-based theorem proving
• Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
• Automated Reasoning
• Coming to terms with quantified reasoning
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Scalable fine-grained proofs for formula processing
• Superposition with lambdas
• The logicist manifesto: At long last let logic-based artificial intelligence become a field unto itself
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Fast and slow enigmas and parental guidance
• Quantifier simplification by unification in SMT
• Vampire with a brain is a good ITP hammer
• Implementing Temporal Logics: Tools for Execution and Proof
• A new methodology for developing deduction methods
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stratified resolution
• Labelled Clauses
• Relational and Kleene-Algebraic Methods in Computer Science
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Alternating two-way AC-tree automata
• KI 2004: Advances in Artificial Intelligence
• Resolution-Like Theorem Proving for High-Level Conditions
• First-order temporal verification in practice
• Simplifying proofs in Fitch-style natural deduction systems
• Superposition with structural induction
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Mechanizing Mathematical Reasoning
• Foundations of Information and Knowledge Systems
• Fingerprint indexing for paramodulation and rewriting
• A resolution-based calculus for preferential logics

This page was built for software: VAMPIRE