Author:Giles Reger

Keyphrases

asynchronous-policy, automated induction, automated reasoning⁶, automated theorem proving², Avatar⁴, AVATAR architecture, Clausal Normal Form, clause splitting, Clausification, combinator, combinatory, complete, connection calculus, Connection tableaux, data race, directed acyclic graph, first-order, first-order logic⁹, first-order theorem prover, first-order theorem proving, gaussian variable elimination rule, Graph Neural Network, grounding mechanism, heuristic search, higher-order², Interpolants, Knuth-Bendix, learned-guidance, local proofs, Logical Entailment, Mizar, parallel theorem proving, parallelism, paramodulation, persistent grounding, Proof attempt, proof checking, proof output, proof search³, quantified event automata, Question Answering, rewriting, rule systems, runtime monitoring, runtime verification, SAT solver, Satisfiability Modulo Theories², Saturation Algorithms², saturation based proof search, saturation-based theorem prover, shared memory, shared persistent grounding, SMT², SMT solving², superposition, superposition calculus, Superpsoition, term ordering, theorem prover², theorem proving⁸, theory reasoning², thread local, Thread Local Storage, Vampire⁸, Z3.