RISC JKU

The proofs are better viewed as Mathematica notebook. If you do not have an installation of Mathematica 4.0 or later, then you can download MathReader free of charge.

New Examples with Predicate Logic Prover

A few examples on some binary relations.

Transitivity of equality (1)
Transitivity of equality (2)
Transitivity of congruence
Symmetric difference (left)
Symmetric difference (right)
  

Sum of limits is the limit of sum

Use of the 4-ary definition of limit
Use of the 3-ary definition of limit
Use the 2-ary definition of limit
  

Two proofs of the same proposition ...

... using PNDLevel 5
... PNDLevel 0
  

Two proofs of '(f+g)(n)=f(n)+g(n)' ...

... using the language without equality ...
... and with.