Simple Proofs
These are small and simple proof example serving the purpose of giving you a first impression of the cut-elimination system CERES.
-
A very simple example of a proof containing a cut rule inference and making use of definition introduction rules:
$ hlk --ceres -o simple2.xml simple2.hlk p$ ceres --cutelim -ac simple2.xml p simple2-ce.xmlSupplemental files: simple2-otter.in (Otter input file) | simple2-otter.out (Otter output file)
-
A slightly modified variant of the previous example:
$ hlk --ceres -o simple3.xml simple3.hlk p$ ceres --cutelim -ac simple3.xml p simple3-ce.xmlSupplemental files: simple3-otter.in (Otter input file) | simple3-otter.out (Otter output file)