Author:Jasmin Christian Blanchette

Publications
EasyChair Preprint no. 396

Keyphrases

automatic theorem provers4, completeness, counterexample generation, direct proofs, first-order logic, higher-order logic3, interactive theorem proving, Isabelle/HOL4, model finding, proof assistant, proof assistants3, prover, resolution2, Satisfiability Modulo Theories (SMT), simple type theory, Skolemization, Sledgehammer2, structured proofs, superposition calculus, Vampire.