Here are some files relevant to a lecture given to the Machine Learning and Reasoning class at the Czech Technical University in Prague.

April 26, 2019.

Two sets of slides

Some input and output files

Here a few introductory examples to illustrate the look and feel of Prover9 and some of its features.

Note that ex5 illustrates an input processing feature and does not prove a theorem.