[go: up one dir, main page]

Larry Wos

What's New

The XCB problem has been solved! On April 13, 2002, at 4:37 p.m., my colleagues and I solved -- in the affirmative -- the XCB open problem in equivalential calculus.

I am working in the area of automated reasoning, developing new strategies and inference rules that can be implemented in automated reasoning programs.  We have made significant gains in automated reasoning in the past few years, as the figure below shows.

For examples of significant challenges (on a Ph.D. level) remaining in the area of automated reasoning, see, for example, "The Problem of Reasoning by Analogy" and "The Problem of Reasoning by Case Analysis."

Current Projects

  • New books
  • A new (December 2003) book about finding new and shorter proofs (somewhat reminiscent of Hilbert's 24th problem) entitled Automated Reasoning and the Discovery of Missing and Elegant Proofs by Larry Wos and Gail W. Pieper
  • A new text about automated reasoning entitled A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning by Larry Wos with Gail Pieper
  • A collection of published papers by L. Wos entitled Collected Works of Larry Wos by Larry Wos with Gail Pieper
  • Elegant proofs
  • One of my most recent successes is the development of the resonance strategy which is useful in particular for finding shorter, more elegant proofs. See An Experimenter's Notebook.
    •
  • New strategies
  • Resonance strategy: is useful in particular for finding shorter, more elegant proofs. See P387.ps.Z "The Resonance Strategy," Computers and Math. with Apps. 29, 2 (1995) 133-178.
  • Hot list: enables the researcher to designate various input clauses as meriting repeated revisiting to complete (rather than initiate) applications of chosen inference rules. The strategy dramatically reduces the CPU time required to reach a desired goal. The hot list strategy was used to find a proof of a theorem in lattice ordered groups that had previously resisted all but the more inventive automated attempts.
  • New methodologies
  • Methodology for finding circles of pure proofs: enables the researcher to find pure proofs (a proof is pure, say, with respect to 3 if the proof that 1 implies 2 does not rely on 3). The methodology was used to find circles of pure proofs for the thirteen shortest single axioms of equivalential calculus. See P479.ps.Z "Searching for Circles of Pure Proofs," The Journal of Automated Reasoning 15, pp. 279-315, 1995.
  • Combinations of strategies
  • Combination of resonance with heat: enables the researcher to find unexpectedly shorter proofs. In a study in two-valued sentential calculus, one highlight was obtaining a 28-step proof of the Frege axiom system, the shortest yet known. See P522.ps.Z "The Power of Combining Resonance with Heat," Journal of Automated Reasoning (to appear).

    • Shorter Proofs

    One of my recent interests is seeking (and finding!) shorter proofs for challenging problems. I encourage researchers to take the files and seek even shorter proofs. Some of the problems are in Boolean algebra, others in quasi-lattices, and still others in equivalential calculus.  See also An Experimenter's Notebook.

    Puzzles

    In response to a frequent request, I have put on the Web a few puzzles that interested students and more advanced researchers may find challenging. The puzzles include the jobs puzzle, the missionaries and cannibals puzzle, the dominoes checkerboard puzzle, the truthtellers puzzle, and the puzzle of fifteen.

    Otter

    Much of the recent success that the Argonne group has enjoyed in automated reasoning is attributable to the powerful reasoning program Otter, developed by W. McCune. Otter has been used to answer numerous challenging questions in mathematics and logic.

    Papers, Reports and Talks

    On-line versions of recent papers

    An Interesting Bio by T. Obermiller

    Addresses

    Mathematics and Computer Science Division
    Argonne National Laboratory
    9700 S Cass Ave
    Argonne, IL 60439

    FAX: 630-252-5986

    [email protected]