VAMPIRE - MaRDI portal

Cited in

(only showing first 100 items - show all)

Combinations of Theories for Decidable Fragments of First-Order Logic
Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories
Large theory reasoning with SUMO at CASC
An introduction to practical formal methods using temporal logic
Relaxed weighted path order in theorem proving
Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
The anatomy of vampire. Implementing bottom-up procedures with code trees
Blocking and other enhancements for bottom-up model generation methods
Restricted combinatory unification
Herbrand constructivization for automated intuitionistic theorem proving
Tools and Algorithms for the Construction and Analysis of Systems
Simple and Efficient Clause Subsumption with Feature Vector Indexing
Automated Reasoning
Heaps and Data Structures: A Challenge for Automated Provers
The logicist manifesto: At long last let logic-based artificial intelligence become a field unto itself
Extending Sledgehammer with SMT solvers
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)
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
Coming to terms with quantified reasoning
Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
Hammering Mizar by Learning Clause Guidance (Short Paper).
AC simplifications and closure redundancies in the superposition calculus
GKC: a reasoning system for large knowledge bases
JGXYZ: an ATP system for gap and glut logics
Logic for Programming, Artificial Intelligence, and Reasoning
Logic for Programming, Artificial Intelligence, and Reasoning
Scalable fine-grained proofs for formula processing
Superposition with lambdas
A neurally-guided, parallel theorem prover
Implementing Temporal Logics: Tools for Execution and Proof
An interactive derivation viewer
A new methodology for developing deduction methods
Automated Reasoning
Simulation and synthesis of deduction calculi
ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
Automated theorem proving in quasigroup and loop theory
SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
Automated search for impossibility theorems in social choice theory: ranking sets of objects
Set-blocked clause and extended set-blocked clause in first-order logic
A navigational logic for reasoning about graph properties
Fast term indexing with coded context trees
scientific article; zbMATH DE number 1943847 (Why is no real title available?)
Presenting and explaining Mizar
Efficient access mechanisms for tabled logic programs
Mechanising first-order temporal resolution
Stratified resolution
Automatic construction and verification of isotopy invariants
AVATAR: The Architecture for First-Order Theorem Provers
Towards Verifying Logic Programs in the Input Language of clingo
Document models
Efficient instance retrieval with standard and relational path indexing
scientific article; zbMATH DE number 2043541 (Why is no real title available?)
scientific article; zbMATH DE number 1765682 (Why is no real title available?)
Labelled Clauses
EUCLID
A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
Extensional higher-order paramodulation in Leo-III
The Relative Power of Semantics and Unification
Relational and Kleene-Algebraic Methods in Computer Science
Alternating two-way AC-tree automata
Lemma Mining over HOL Light
TPTP, TSTP, CASC, etc.
SMELS: Satisfiability Modulo Equality with Lazy Superposition
Harald Ganzinger's legacy: contributions to logics and programming
Verifying Tight Logic Programs with anthem and vampire
scientific article; zbMATH DE number 7350767 (Why is no real title available?)
Automated Reasoning
First-order temporal verification in practice
Simplifying proofs in Fitch-style natural deduction systems
Towards satisfiability modulo parametric bit-vectors
KI 2004: Advances in Artificial Intelligence
Predicate Elimination for Preprocessing in First-Order Theorem Proving
Superposition with structural induction
Portfolio theorem proving and prover runtime prediction for geometry
Semantically-guided goal-sensitive reasoning: inference system and completeness
Resolution-Like Theorem Proving for High-Level Conditions
scientific article; zbMATH DE number 5850137 (Why is no real title available?)
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
scientific article; zbMATH DE number 1765674 (Why is no real title available?)
Practical solution techniques for first-order MDPs
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
Decidable Fragments of Many-Sorted Logic
A resolution-based calculus for preferential logics
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
Interpolation and Symbol Elimination
Mechanizing Mathematical Reasoning
Fingerprint indexing for paramodulation and rewriting

This page was built for software: VAMPIRE