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, CEGAR, Clausal Normal Form, clause elimination, clause normal form, Clausification, EPR, finite model finder, first-order logic7, first-order theorem proving, FOOL, inprocessing techniques, Interference, Interpolants, IRM-calc, local proofs, long-distance resolution, machine learning, Parameters Learning, partial strategy, Preprocessing, proof checking, proving strategy, QBF, QBF calculi, Resolution Calculi, SAT2, SAT solving, Satisfiability Modulo Theories2, Saturation Algorithms2, semantics2, SMT, SMT solving2, strategies, strategy invention, superposition calculus, theorem proving8, theory reasoning, translation, Vampire6, winning strategy, Z3.