Pecan: An Automated Theorem Prover

Pecan is an automated theorem prover. You can view the manual (which is currently rather incomplete) here. Below, you can enter a program and click "Run" to try out Pecan; there are several example programs you can try out. There are some limitations: some features of Pecan are not available, your programs must be under \(10^5\) characters, and your programs will time out after 5 minutes. If that's too limiting, you should look into installing Pecan on your own computer. Instructions are available at the repository: If you use Pecan in your research, please cite this paper
Enter a Pecan program below:

This website is written in Prolog