From: Vincenzo Iozzo To: "Jeffrey E." <jeevacation@gmail.com> Subject: Fwd: SMT Solvers for legal code Date: Wed, 17 Feb 2016 04:45:32 +0000 Sent from my Iphone Begin forwarded message: From: Vincenzo Iozzo Date: February 17, 2016 at 13:43:17 GMT+9 To: Joichi Ito Cc: Alexander Lourie Subject: SMT Solvers for legal code Ok so as you probably remember I've been rewriting the language used in the cyber export control stuff for the Wassenaar agreement. And I noticed an amusing thing: policy people and lawyers like the "unpacking" of clauses. Essentially you take something like: 4.e.l.a "technology" according to the General technology note for the "development", "production" or "use" of equipment or "software" specified by 4.D 4. D "software" specially designed or modified for the generation, operation or delivery of, or communication with, "intrusion software" And you unpack them to: "Technology" "required" (Le 'peculiarly responsible for achieving or exceeding the controlled performance levels, characteristics of functions) for the "development", "production" or "use" of [4.D "Software" specially designed or modified for the generation, operation or delivery of, or communication with, "intrusion software") Now there are these things called "SMT solvers" (satisfiability modulo theory) that are essentially fancy calculators based on theories. Eg: you take the rules of real numbers or the rules of geometry or the rules of how strings work inside computers, then you take formulas/sentences that are supposed to operate in the theory and you verify whether the formula/sentence is satisfiable or not. Example: "for every Y and for every X such that X = Y + 1, Y*X is even" would tell you that is SAT in the integer theory but not in the real (numbers) theory So I was half jokingly thinking: what if somebody built a SMT solvers for legal stuff? And more importantly: what if you used an SMT solver to make your case in court? Essentially this would be "the letter of the law" on steroids, but you could also prove the inconsistency of it and then argue that the "spirit of the law" is bullshit if the letter is inconsistent? EFTA00834259 Joi, The ML should do that! I will gladly help both in the building phase and in the testing phase (Sandy, for the testing phase I need all your pro bono time though :p) Sent from my Iphone EFTA00834260