Theorem proving and patents ...

Patents are supposed to be formal specifications of inventions that contain enough information for someone reasonably skilled in the art to reproduce the invention. I'm curious as to whether anyone is working on automating patent comparisons for the purpose of establishing violations. My shallow understanding is that proving systems might have something to contribute to that problem, or at least a significant enough subset of it - at least for "software patents".

Having such a system might be a good weapon against big firms that file suits that take ages to verify and primarily serve to feed the pockets of lawyers (apologies for the cynicism there).

policy, law

Vicky Weissman [http://www.cs.cornell.edu/People/vickyw/] stated interest in modeling legal policies a couple of years ago, though I don't know what she ended up thinking about. In a talk, she described different people translating the same laws into logically different policies, even when transcribing into a severely limited policy language. The confluence of statistical nlp, theoretical linguistics, and formal logic is beastly - her work demonstrated the logical level has its own sea of obvious conundrums, even without the subjective and contextual imprecision of intended meaning. I'm sticking with web & media language design for now :)

- Leo

By lmeyerov at Sun, 2006-12-17 08:42 | login or register to post comments

The first thing we do...

Having such a system might be a good weapon against big firms that file suits that take ages to verify and primarily serve to feed the pockets of lawyers (apologies for the cynicism there).

So instead, suits will take ages to verify and primarily serve to feed the pockets of a newly wealthy group of formal specification gurus? Sign me up! ;)

Seriously, it seems to me that proving an equivalence (or otherwise) between formal descriptions of two different patents would be non-trivial, at best.

By Anton van Straaten at Sun, 2006-12-17 09:53 | login or register to post comments

Formalization

You will also be left with the fuzzy problem of translating the informal into a formal language. Even if you could formally prove equivalence between two formalized patent descriptions, there'd always be room for argument about the formalization process itself. At which point the lawyers would get invovled again.

By Allan McInnes at Sun, 2006-12-17 20:42 | login or register to post comments

Law and Logic

As an attorney, let me say that in my personal opinion (this isn't a formal position of The Institute for End User Computing, Inc.), Software Patents are a very Bad Thing that have ceased to have any connection to the original goals of the Patent System, which was predicated on the assumption that no one would innovate absent the economic lure of using the time limited patent monoploy to recover royalty payments from licensees and that issuing such a monopoly would be necessary to get people to publish their discoveries.

Today's product lifecycles, particularly in software, are so much shorter than they were at the time the system was set up that the time period is effectively far longer than the Founders intended.

Likewise, the language of patent applications effectively renders them unintelligible to most practioners of the art who often have far stronger academic motivations for publishing far more intelligible disclosures of their innovations.

Moreover, the cost of procuring Patents is so high as to put them out of reach of most individuals, making them far more effective as a tool to surpress technical competition.

As to formalizing legal documents, I would have to say that most lawyers can't deal with formal represenations. Back when I was in Law School we had a short lived attempt to get law students to encode legal arguments in Prolog. If you Google for Law and AI you can find work related to such issues.

This sort of automation works if applied to drafting statutes and contracts where you can constrain the domain of discourse and build up a suitble ontology. However, patents are by definition open ended, so trying to create a formal language to cover them all would be an intractable problem. In short, when trying to formalize law, you have to think in terms of semi-structured information.

But if you really want to improve the patent system, you'd do far better to educate lawyers about the software industry, CS in academia, and the open source software development community.

All that formalizing the patent filings will do is to increase their costs and add a whole new Tar Pit for us to wade through; indeed, filings are already quite effectively indexed for those with expertise in searching the system. The real source of bad, overly expansive patent claims is failure to bring in Prior Art early on and an organizational bias at the PTO to issue as many patents as possible as quickly as possible.

By Peter J. Wasilko at Sun, 2006-12-17 20:21 | login or register to post comments

On software patents...

There is one more purpose that patents serve - a small company might invent something, but might not have the muscle to bring the invention to the society in full glory. A larger company might have that muscle. Having the invention patented helps the small company claim legal entitlement to some of the profits of the larger company that were due to the invention they copied. This is reasonable for software patents as well.

I'm not sure whether software patents should be illegal as long as control system patents are legal.

The difference between software patents and other patents I'd like to see is the requirement of full disclosure of documented source code and binaries of a working invention. Its quite pointless writing pages of formal documentation of software when its source code will speak for itself. And it'll help to explicitly relate each claim to a set of sections of the source code if possible.

Once source code is made a requirement, formal verification processes can step in to some extent without having a patent ontology and a separate formal specification language for patents. Free text data mining combined with program equivalence might be able to help in patent violation situations.

Automated tools will never be the full story, but their analysis results can form a substantial part of evidence, help in determining damages, etc.

Maybe my naivette makes me see the possibilities, however hard a problem this is :)

By Srikumar Subramanian at Sun, 2006-12-17 23:44 | login or register to post comments

Copyright v. Patent

Having the invention patented helps the small company claim legal entitlement to some of the profits of the larger company that were due to the invention they copied. This is reasonable for software patents as well.

I must point out a subtle distinction between Copyright and Patent here.

Patent law has nothing to do with copying! It is a negative right that lets the holder prevent someone from using a technology even if they invented it with no knowledge of your claims at great expense to themselves. Moreover, even if you hold a patent, you might not be able to use your technology if someone else claims a patent to some piece of what you are doing.

The big company in your scenario would probably be able to make multiple claims against your small company which, even if frivolous, would bankrupt you long before you win in court. Patents are a game for big deep pocketted players who can afford teams of lawyers. So the only way your small company would win is to fund an extremely expensive lawsuit yourselves or to sell out your equity to get the capital needed to win the suit at which point it isn't your company any more.

Goggle for "The Patent Thicket" to learn more about these issues.

Copyright law covers outright copying of your code, even with minor mods and under the rules of Discovery you could get to see the big company's source code to perform the analysis you contemplate under today's law. It is far less expensive and more appropriate for small software houses.

Bottom Line: Copyright Good, Patent Bad!

Please note that nothing in this post is intended to offer specific legal advice and that you should always consult an Intellectual Property attorney in your jurisdiction before choosing a form of IP protection. Also the views in this post are those of Peter J. Wasilko, Esq. and are not official positions of The IEUC.

By Peter J. Wasilko at Mon, 2006-12-18 14:48 | login or register to post comments

I too am coming to the

I too am coming to the conclusion that copyright law is sufficient for the software industry in general, but there are some areas where patents still seem to make sense - as a last resort weapon.

So the only way your small company would win is to fund an extremely expensive lawsuit yourselves or to sell out your equity to get the capital needed to win the suit at which point it isn't your company any more.

This is exactly the scenario I'm hoping some tool might help prevent.

Software has this property that often an "invention" that is really novel, useful and non-obvious, suddenly becomes obvious after it becomes known. It can also be reverse engineered witout having access to the source code of the invention by sheer guessing most of the time - my analogy with control systems holds here. In this case, having formal tools to establish connections between software (copyright wise or patent wise), given that their source code might not have any symbolic connection at all, does seem to be of some value.

Anyway, I was interested in the problem I stated more than in debating copyright vs patents. I'm not really qualified for that debate and hold a fairly narrow understanding of the issues involved.

By Srikumar Subramanian at Mon, 2006-12-18 22:33 | login or register to post comments

Lambda the Ultimate

User login

Navigation