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, linear arithmetic, local proofs, Logical Entailment, Mizar, parallel theorem proving, parallelism, paramodulation, persistent grounding, Proof attempt, proof checking, proof output, proof search³, quantified event automata, Quantified First-Order Logic, 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.