About
About Empty Clause
Who this site is for, what it covers and what it is not.
What this site is
Empty Clause is an independent educational site about automated theorem proving and the logic behind it. It explains resolution, first-order logic, the TPTP problem format, the CASC competition, the relationship between SAT, SMT and first-order provers, and the role of proof assistants.
It is not the website of a theorem prover, a research group, a competition or a conference, and it is not affiliated with any of them. Names of programs and events appear only to describe them for readers.
How the texts are written
Articles stick to well-established facts such as published rules, standard formats and widely documented results. Where an area is still debated, or where figures change from year to year, the text says so and points readers to the official pages of the project concerned.
Please check the official documentation before relying on any detail for research or software work. Rules, versions and results are updated by their maintainers.
What you will not find here
There are no downloads, no accounts and no forms. The site does not publish software, benchmark results of its own or advice that replaces a textbook.