Author:Konstantin Korovin
Keyphrasesabstraction refinement, arithmetic, automated reasoning, automated theorem proving, Bounded Model Checking, Clause Evaluation, EPR, EPR fragment, first-order logic, Graph Neural Networks, interpolation, k-induction, linear arithmetic, machine learning, Quantified First-Order Logic, SMT2, theorem proving3, unification, Unification with Abstraction. |