This website summarizes the experiments conducted for the paper Certified Equational Reasoning via Ordered Completion by Christian Sternagel and Sarah Winkler.
Below you can find three kinds of experiments:
The results of CTRS experiments are available in the table below. In the table, Cops numbers are hyperlinked to the corresponding input and answers to proofs (pretty printed CPF certificates in case of "-cert" columns and plain text files, otherwise). The two new problems mentioned in our paper are 340 and 361.
Furthermore, we provide a ZIP archive with all required (Linux) binaries and scripts to reproduce our experiments. (See also the corresponding README.)
The table below summarizes the results of our ordered completion experiments. File names are hyperlinked to the corresponding input and answers to proofs (pretty printed CPF certificates in case of "cert" columns and plain text files, otherwise).
Furthermore, we provide a ZIP archive with all required binaries and a README that describes how to reproduce our experiments.
The table below summarizes the results of our ordered completion experiments. File names are hyperlinked to the corresponding input and answers to proofs (pretty printed CPF certificates in case of "cert" columns and plain text files, otherwise).
Furthermore, we provide a ZIP archive with all required binaries and a README that describes how to reproduce our experiments.
| TPTP | cert | noncert |
|---|---|---|
| ALG299-1 | YES | YES |
| ALG300-1 | YES | YES |
| ALG302-1 | YES | YES |
| BOO027-1 | YES | YES |
| GRP393-2 | YES | YES |
| GRP394-3 | YES | YES |
| HWC004-1 | YES | YES |
| HWC004-2 | YES | YES |
| LCL407-2 | YES | YES |
| LCL905-1 | YES | YES |
| SYN552-1 | YES | YES |