Author:Martin Suda

Keyphrases

automated reasoning⁴, automated theorem proving³, Avatar⁴, AVATAR architecture, blocked clauses, CEGAR, Clausal Normal Form, clause elimination, clause normal form, Clause selection, Clausification, conjecturing, E prover, EPR², evaluation, finite model finder, first-order logic⁷, first-order theorem proving², FOOL, Graph Neural Network, higher-order, inprocessing techniques, Interference, Interpolants, IRM-calc, ITP hammers, large theory problems, lemma introduction, local proofs, long-distance resolution, machine learning³, Mizar, neural clause-selection guidance, Parameters Learning, partial strategy, premise selection, Preprocessing, proof checking, proving strategies, proving strategy, PSPACE, QBF², QBF calculi, randomization, Resolution Calculi, SAT², SAT solving, Satisfiability Modulo Theories², Saturation Algorithms², saturation-based theorem proving³, Schaefer fragments, semantics², sine, SMT, SMT solving², strategies, strategy invention, Strategy Scheduling, superposition, superposition calculus, theorem proving⁸, theory reasoning, translation, Vampire¹⁰, winning strategy, Z3.