Author:Liron Cohen
Keyphrasesautomated reasoning, completeness, computability, Coq, cyclic proofs, Digital Library, Free choice sequences, geometry, Herbrand structures, induction, infinitary proofs, Intuitionistic mathematics, Kripke semantics, monotonicity, Nuprl2, projective plane, proof checker, sequent-based proof systems, transitive closure, type theory, Verified theorem prover backend. |