Proofs in natural language contain much information useful for automatic proof checking that is usually lost in translation to a formal language. This paper describes a system which checks English language proofs in elementary number theory that uses such information to guide the theorem prover. The proof connector follows the argument presented in the proof and asks a theorem prover to make the same deductions that the human reader of the proof is assumed to make. This system has the added advantage of spotting fallacious proofs of correct theorems. A more powerful theorem prover might prove the theorem by ignoring a faulty proof.

Summary. The determination of evolutionary relationships is a fundamental problem in evolutionary biology. Genome arrangement data are potentially more informative than deoxyribonucleic acid sequence data for inferring evolutionary relationships between distantly related taxa. We describe a Bayesian framework for phylogenetic inference from mitochondrial genome arrangement data using Markov chain Monte Carlo methods. We apply the method to assess evolutionary relationships between eight animal phyla.

We further develop the Bayesian framework for analyzing aligned nucleotide sequence data to reconstruct phylogenies, assess uncertainty in the reconstructions, and perform other statistical inferences. We employ a Markov chain Monte Carlo sampler to sample trees and model parameter values from their joint posterior distribution. All statistical inferences are naturally based on this sample. The sample provides a most-probable tree with posterior probabilities for each clade, information that is qualitatively similar to that for the maximum-likelihood tree with bootstrap proportions and permits further inferences on tree topology, branch lengths, and model parameter values. On moderately large trees, the computational advantage of our method over bootstrapping a maximum-likelihood analysis can be considerable. In an example with 31 taxa, the time expended by our software is orders of magnitude less than that a widely used phylogeny package for bootstrapping maximum likelihood estimation would require to achieve comparable statistical accuracy. While there has been substantial debate over the proper interpretation of bootstrap proportions, Bayesian posterior probabilities clearly and directly quantify uncertainty in questions of biological interest, at least from a Bayesian perspective. Because our tree proposal algorithms are independent of the choice of likelihood function, they could also be used in conjunction with likelihood models more complex than those we have currently implemented.

A problem that comes up in any proof-checking system is whether or not a proof step is a valid instantiation of a lemma or theorem. Often, the lemma or theorem may include set variables and so in general can be second order. This problem is somewhat simpler than the more general problem of second order unification. Jensen and Pietrzykowski [1] and Huet [2] give semi-decision procedures for finding ω-order unifiers. The second order instantiantion problem is shown to be NP-complete in Baxter [3]. Our approach will be to find useful subcases of the second order instantiantion problem which yield to fast algorithms. This paper is a first approximation towards that goal.

Course Objectives: We will discuss modern techniques in automated theorem proving. Theorem provers can be used as mathematical assistants, to verify programs, and to check hardware specifications. We will begin with the necessary background in logic, namely proposition and predicate calculus. We will discuss natural deduction systems as well as resolution. Other topics will include: model checking, binary decision diagrams, modal and higher-order logics, and Bayesian decision networks. The course will emphasize the use of computer tools for proving theorems and verification.