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
