Author:Andrei VoronkovPublications |
---|
EasyChair Preprint no. 5000 | EasyChair Preprint no. 2468 | EasyChair Preprint no. 3169 | EasyChair Preprint no. 3148 | | EasyChair Preprint no. 826 | | EasyChair Preprint no. 98 | EasyChair Preprint no. 1 | | | | | | | | | | | | | | | | | | | |
Keyphrasesautomated induction, automated reasoning6, automated theorem prover, automated theorem proving2, Avatar3, AVATAR architecture2, bounded quantifiers, Clausal Normal Form, clause normal form, Clausification, code trees, computability, conference management, easychair, first-order logic6, first-order theorem prover, first-order theorem proving3, FOOL, fool formula, forward subsumption, gaussian variable elimination rule, hereditarily finite sets, induction, induction with generalization, interpolation, logic programming, next state relation, program verification, proof search, Resolution Calculus, runtime algorithm specialization, SAT solving, Satisfiability Modulo Theories2, Saturation Algorithms3, saturation based proof search2, SMT2, SMT solving, static analysis, structural induction, Subsumption algorithm, superposition, superposition calculus, superposition reasoning, term algebra, term indexing, theorem prover2, theorem proving4, theory reasoning2, translation, Vampire6, Web Services, Z3. |
|