ESP Wiki is looking for moderators and active contributors!
Stålmarck's algorithm
Stålmarck's algorithm, which describes a decision procedure, is covered in the USA by patent [1]. It is often considered that all "saturation based decision procedure" is claimed by the patent.
Academic papers explicitly note its patented status: in 1996, in 2000, etc. It is notable that the algorithm actually was never properly published, so academic publications often cite the patent itself. The alternative is to cite the unpublished manuscript.
The algorithm is important enough that the standard handbook of the field, Handbook of Practical Logic and Automated Reasoning (published 2009), devotes nearly 10 pages to the algorithm. As usual, the book notes its patented status on page 90.
