VAMPIRE

swMATH2918MaRDI QIDQ15455

No author found.

Related Items (only showing first 100 items - show all)

Fast term indexing with coded context trees ⋮ Heterogeneous heuristic optimisation and scheduling for first-order theorem proving ⋮ Inductive benchmarks for automated reasoning ⋮ Automated generation of exam sheets for automated deduction ⋮ MaLeS: a framework for automatic tuning of automated theorem provers ⋮ MizAR 40 for Mizar 40 ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Fast and slow enigmas and parental guidance ⋮ Vampire with a brain is a good ITP hammer ⋮ Quantifier simplification by unification in SMT ⋮ Theory exploration powered by deductive synthesis ⋮ Practical solution techniques for first-order MDPs ⋮ ATP-based cross-verification of Mizar proofs: method, systems, and first experiments ⋮ Towards finding longer proofs ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ The role of entropy in guiding a connection prover ⋮ Eliminating models during model elimination ⋮ Learning theorem proving components ⋮ First-order temporal verification in practice ⋮ Simplifying proofs in Fitch-style natural deduction systems ⋮ A learning-based fact selector for Isabelle/HOL ⋮ The anatomy of vampire. Implementing bottom-up procedures with code trees ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Things to know when implementing KBO ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ Multi-completion with termination tools ⋮ Towards a unified ordering for superposition-based automated reasoning ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Hammer for Coq: automation for dependent type theory ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ Superposition-based equality handling for analytic tableaux ⋮ Symmetry avoidance in MACE-style finite model finding ⋮ A neurally-guided, parallel theorem prover ⋮ Herbrand constructivization for automated intuitionistic theorem proving ⋮ Introducing \(H\), an institution-based formal specification and verification language ⋮ Superposition with structural induction ⋮ On combining algebraic specifications with first-order logic via Athena ⋮ Stratified resolution ⋮ Limited resource strategy in resolution theorem proving ⋮ Model evolution with equality -- revised and implemented ⋮ Property-directed inference of universal invariants or proving their absence ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Document models ⋮ Relaxed weighted path order in theorem proving ⋮ Induction with generalization in superposition reasoning ⋮ Automatic construction and verification of isotopy invariants ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas ⋮ Making theory reasoning simpler ⋮ Combined reasoning by automated cooperation ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ A navigational logic for reasoning about graph properties ⋮ The logicist manifesto: At long last let logic-based artificial intelligence become a field unto itself ⋮ Resolution is cut-free ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ From LCF to Isabelle/HOL ⋮ Machine learning guidance for connection tableaux ⋮ ProofWatch: watchlist guidance for large theories in E ⋮ Inspection and selection of representations ⋮ Superposition for \(\lambda\)-free higher-order logic ⋮ A generic framework for implicate generation modulo theories ⋮ Superposition with datatypes and codatatypes ⋮ A FOOLish encoding of the next state relations of imperative programs ⋮ MædMax: a maximal ordered completion tool ⋮ A resolution-based calculus for preferential logics ⋮ An abstraction-refinement framework for reasoning with large theories ⋮ Lightweight relevance filtering for machine-generated resolution problems ⋮ Solving the \$100 modal logic challenge ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Combining induction and saturation-based theorem proving ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ Integer induction in saturation ⋮ Neural precedence recommender ⋮ Handling transitive relations in first-order automated reasoning ⋮ Automated verification of refinement laws ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ A new methodology for developing deduction methods ⋮ Unprovability results for clause set cycles ⋮ Induction and Skolemization in saturation theorem proving ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Subsumption demodulation in first-order theorem proving ⋮ Layered clause selection for theory reasoning (short paper) ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A Wos Challenge Met ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Theorem proving as constraint solving with coherent logic ⋮ Verifying Whiley programs with Boogie ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ Ground joinability and connectedness in the superposition calculus ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description) ⋮ Evaluating general purpose automated theorem proving systems

This page was built for software: VAMPIRE