Programming and verifying a declarative first-order prover in Isabelle/HOL. - Jensen, Alexander Birch; Larsen, John Bruntse; Schlichtkrull, Anders; Villadsen, Jørgen; Fontaine; Kaliszyk; Schulz; Urban (AI Communications, 2018)