HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)

Future Work

We plan to develop the following extensions of CERES:

To demonstrate the abilities of CERES and the feasibility of formalizing and analyzing complex proofs of mathematical relevance, we currently investigate Fürstenberg's well known proof of the infinity of primes using topology (which may be found in "Proofs from THE BOOK"). The refutations of the characteristic clause set of the problem reflected some of the well-known prime constructions (in particular also Euclid's one).