<div dir="ltr">Can't we formally proof something as obvious Adam's case?</div><div class="gmail_extra"><br><div class="gmail_quote">2016-01-27 10:51 GMT+01:00 Pavel Velikhov <span dir="ltr"><<a href="mailto:pavel.velikhov@gmail.com" target="_blank">pavel.velikhov@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5"><br>
> On 27 Jan 2016, at 12:37, Christian Grün <<a href="mailto:christian.gruen@gmail.com">christian.gruen@gmail.com</a>> wrote:<br>
><br>
>> Its a common practice for everybody, who needs to come up with formal proofs. You start with the most simplified definitions possible, that capture the essence of the problem.<br>
>> Then you get the skeleton of the proof that is hopefully very simple. Then you can add details back, hoping that the proof remains simple and tractable.<br>
>><br>
>> So imagine starting the proof while considering all the possible variations of path expressions, all the Infoset stuff, all XML Schema details. I think its hopeless.<br>
><br>
> I’m completely in line with Michael’s observations. It would obviously<br>
> be nice to have proofs for the full rule sets of the discussed<br>
> languages; but as experience shows, no one will do it (the rare<br>
> exception might prove the rule), so we are stuck with the work that is<br>
> of limited practical use.<br>
<br>
</div></div>I can’t agree with you. There are a lot of results that automatically hold for the full specification, even though they are<br>
proved on a clean and easy-to-use subset: undecidability and np-completeness or np-hardness for instance.<br>
<br>
For the full specifications its sometimes hard to grasp the semantics, so proving anything serious is impossible.<br>
Example: try proving that SQL-2003 queries are equivalent to some superset of relational algebra.<br>
<br>
</blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div>
<p> 
W.S. Hager<br>
Lagua Web Solutions<br>
<a href="http://lagua.nl/" target="_blank">http://lagua.nl</a><br></p></div></div>
</div>