ESP Wiki is looking for moderators and active contributors!
Difference between revisions of "Stålmarck's algorithm"
(publication date) |
(small changes to intro to separate the algorithm from the patent) |
||
Line 1: | Line 1: | ||
− | [http://www.google.com/patents/ | + | Stålmarck's algorithm, which describes a decision procedure, is covered in the [[USA]] by patent [http://www.google.com/patents/US5276897US-5276897-A]. It is often considered that all "saturation based decision procedure" is claimed by the patent. |
− | Academic papers explicitly note its patented status: [http://www.cl.cam.ac.uk/~jrh13/papers/stalmarck.html in 1996], [http://dl.acm.org/citation.cfm?id=594285 in 2000], etc. It is notable that the algorithm actually was never properly published, so academic publications | + | Academic papers explicitly note its patented status: [http://www.cl.cam.ac.uk/~jrh13/papers/stalmarck.html in 1996], [http://dl.acm.org/citation.cfm?id=594285 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, [http://books.google.co.kr/books?id=lYSYLPWJQKMC 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 [http://books.google.co.kr/books?id=lYSYLPWJQKMC&pg=PA90 page 90]. | |
==Related pages on {{SITENAME}}== | ==Related pages on {{SITENAME}}== |
Latest revision as of 11:45, 25 April 2015
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.