Author:Martin Suda

Publications
EasyChair Preprint no. 362
EasyChair Preprint no. 361
EasyChair Preprint no. 1

Keyphrases

automated reasoning4, automated theorem proving2, Avatar4, AVATAR architecture, blocked clauses, Clausal Normal Form, clause elimination, clause normal form, Clausification, first-order logic7, first-order theorem proving, FOOL, Interpolants, IRM-calc, local proofs, long-distance resolution, machine learning, Parameters Learning, partial strategy, Preprocessing, proof checking, proving strategy, QBF, QBF calculi, Resolution Calculi, SAT, Satisfiability Modulo Theories2, Saturation Algorithms2, semantics2, SMT, SMT solving2, strategies, strategy invention, superposition calculus, theorem proving8, theory reasoning, translation, Vampire6, winning strategy, Z3.