Michael Jones, PhD: May 2004 Archives

« April 2004 | Main | June 2004 »

May 25, 2004

[Misc.] Little Wild Horse Canyon with twins

[little wild horse] A fun first camping trip with one year old twins. Includes a slightly adventerous but stunning hike in a world-class canyon will beautiful narrows. I wouldn't do it any later than May due to heat, but highly reccomended otherwise.

We camped on wide open BLM land between Goblin Valley and LIttle Wild Horse. That worked out well because there was nobody around to hear the girls scream, I mean, cry at night etc. ;) Camping in the park, with lots of neighbors in close proximity, would have been more stressfull. We brought tons of water and strapped the twins' booster seats to the tailgate of the truck for feeding. Worked great (see picture at website above).

Little wild horse is a fun slot canyon for packing two babies. The narrows are spectacular and not very far in. There is one scrambling obstacle early in the canyon. On the way in, we climbed out of the canyon and around the obstacle. Descending back into the canyon was more difficult than the obstacle due to loose dirt and steepness. On the way out, we went down the obstacle with twins' on our backs. No problem. Getting up will probably require passing baby carriers over the obstacle.

The narrows were alot of fun and the twins seemed to enjoy them. They liked to feel the sandstone. We brought their favorite sippy cups and forced water down them at every stop.

We ran into another set of twins and their parents. They were 4 year old girls being packed by their parents.. Those parents seemed to be having a great time too.

Posted by jones at 09:34 AM | Comments (0)

May 19, 2004

[Research] Tic tac toe example from SPIN

[Tic Tac Toe Example] the tic tac toe example from Holzmann's spin 2004 paper.

Posted by jones at 10:10 AM | Comments (1)

May 18, 2004

[Research] embedded C code in SPIN

[The SPIN MODEL CHECKER -- Primer and Reference Manual] Of particular interest is chapter 17 which describes how to embed C code. Fortunately, this chapter is online since there were some formatting issues at the publisher. Our library has a copy of the book, but it seems to be missing ?!

Posted by jones at 03:36 PM | Comments (0)

May 14, 2004

[Research] SPIN distribution (for MAC too)

[Spin - Version 4.1 - April 2004] Installation as described, so far.

Posted by jones at 11:24 AM | Comments (0)

May 13, 2004

[Tech Support] Change bars in latex

[CTAN directory: /tex-archive/macros/latex/contrib/changebar/]

Posted by jones at 01:24 PM | Comments (0)

May 12, 2004

[Tech Support] really basic shell programming

[bash, tests] note that the spaces in the guard of an if statement are essential. So nice to work in an old, dead language.

Posted by jones at 10:28 AM | Comments (0)

May 11, 2004

[Tech Support] How to clip an eps in latex

How to clip a eps figure in latex.

At the terminal...
> ps2epsi foo.ps > eps2eps foo.epsi foo.eps
shorter solutions may exist. Find them if you care.
\begin{figure*} \begin{center} % \epsfysize=3.0in % \epsfbox[55 519 438 ]{bf-corrected.eps} \epsfig{file=figs/expl-bayes.eps,width=4.0in,bbllx=63,bblly=430,bburx=594,bbury=711} \end{center} \caption{Using the empirical Bayes method to revise cost estimates. Although node $s$ has a lower estimated cost than node $b$, the revised cost for $s$ is higher due to the higher mean cost and cost variance of $b$'s siblings.} \label{fig:bayes} \end{figure*}

Posted by jones at 01:30 PM | Comments (0)

May 10, 2004

[Research] Counter Logic with Uninterprected Functions (CLU)

[Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions - Bryant, Lahiri, Seshia (ResearchIndex)] An interesting logic to which AtelierB's predicate prover can be compared.

CLU allows arithmetic expressions, functions from int to int, frunctions from int to bool and successor. I bet we could have done most of our proofs in CLU. The question is: how many CLU proofs wouldn't have been found using the PP in AtelierB?

Posted by jones at 03:10 PM | Comments (0)

[Research] Details about AtelierB's Predicate Prover

[Click-n-prove] Scrounging up some details about the predicate prover and other aspects of AtelierB.

From Dominique's TPHOLs 2003 paper: " The prover pp is more elaborate than pb, it is based on a firmer theoretical background: it is essentially a prover for First Order Predicate Calculus with Equality (and some Arithmetic) together with a Translator from Set Theory to First Order Predicate Calculus. "

This is an interesting statement from the same paper:

In no way is pp constructed from a meta-prover able to be parameterized by a variety of distinct logics. This contrasts with what can be seen in academic circles where extremely powerful general purpose Proof Systems are usually offered: HOL [8], Isabelle [12], PVS [11], Coq [5], etc. Our approach is quite different. It is rather similar to that used in the development of some industrial programs handling symbolic data. For instance, a good C compiler is not a meta-compiler specialized to C; likewise, a good chess-playing program is not a general purpose game-playing program specialized by the rules and strategies of the game of chess.

We think that it is important to completely separate these two functions in two distinct tools: again, this is what is done in Atelier B where you have the, so-called, Proof Obligation Generator based on a weakest pre-condition analysis of formal texts and which delivers the statements to be proved (it tells you the “what-to-prove”), and, as a distinct tool, the Prover which is supposed to discharge the previous statements (it tells you thus the “how-to-prove”). Our view is that, whatever the logic of system development you decide to use, it will generate some final lemmas that are, inevitably, to be proved within classical logic.

Moreover, we do not think at all that the usage of Set Theory restricts you to the expression of elementary mathematical facts only: it is quite possible to encode within Set Theory mathematical statements that are clearly belonging to what is called higher order logic [1] (another example is given in Appendix 2).

Some more details on the predicate prover: "The prover pp essentially first contains a decision procedure for Propositional Calculus. This procedure is very close to what is elsewhere proposed under the technical name of Semantic Tableaux [7]. "

The prover has two steps that are repeated. First, rewrite terms involving universal quantifiers into terms that have a contradiction on the right side of the sequent. If that fails, then you have to instantiate some universally quantified terms to get a contradiction with the literals. That's next. Second, do some instantation of the quantified variables to derrive a contradiction. This is done using something like the "set of support" method in Otter[10]. There's an example in the paper.

The main limitations of the prover are that... 0. Its sensitive to useless hypotheses. For good or bad. 1. its not good at abstracting a statement into a previously proven but more general statement. 2. doesn't manage equality very well. 3. Isn't good at things where you have to creatively make a decision on how to proceede with the proof. This is endemic to automatic provers everywhere.

References:
[1] J.-R. Abrial, D. Cansell, and G. Lafitte. "Higher-Order" Mathematics in B. In ZB’2002 – Formal Specification and Development in Z and B, number LNCS 2272 in Lecture Notes in Computer Science, pages 370–393, 2002.
[7] M. Fitting. First-order logic and automated theorem proving (2nd ed.). Springer-Verlag New York, Inc., 1996.

Posted by jones at 02:42 PM | Comments (0)

[Research] International NSF programs

[International Opportunities for Scientists and Engineers nsf03559] The proposal is cooking right along for May submission...

Be sure to address these "issues of special importance"

Research objectives and methodology.
Description of cooperative arrangement/division of labor/complementary expertise.
Details on the scientific significance of the host country/counterpart institution.
Information about the significant expertise of the foreign partner(s).
Information on the history of collaborative efforts with foreign counterpart, if any.
Expected scientific/engineering and mutual international benefits to be derived from the cooperative arrangement.