The Modal Logic $100 Challenge

Logic provides a rich source of challenges, to determine the relationships between different logics, and between different axiomatizations of the same logic. In modal logics, the lattice of relationships between the Kripke based logics up to S5 is a well known structure. These relationships have been established over the years using a variety of techniques. Each logic in such a lattice has a basis, consisting of a set of axioms and a suite of inference rules. Theorems of the logic are the axioms, and any theorems that can be derived from prior theorems using the inference rules. There are three possible relationships between two logics, or two axiomatizations of one logic:

The logics are equivalent - they have the same theorems. For example, the KM4B axiomatization of the modal logic S5 is equivalent to the KM5 axiomatization.
One logic is stronger than the other - the theorems of the first are a strict superset of the theorems of the other. For example, modal logic S5 is stronger than S4.
The logics are incomparable - each has some theorems that the other does not. For example, modal logic K is incomparable with S1.

Consider the lattice of logics shown in the header of this page (click on either image for an enlarged view). It shows some of the ways the logics (the nodes) can be built from each other by the addition of appropriate axioms or rules (the edges). The axioms and rules of the logics are provided on John Halleck's Logic Systems WWW pages:

PC (for the $100 challenge described below, you may choose any one of the listed axiomatizations: the Principia axioms, Hilbert's PPL + some axiom(s), the Lukasiewicz axioms, or the Rosser axioms).
K (PC + axiom K + necessitation)
S0.5 (PC + axiom K + axiom N")
VER (K + axiom VER)
T (aka M) (K + axiom T)
S1⁰
S1 (S1⁰ + axiom M6)
S3 (S1 + axiom S3)
TRIV (S3 + axiom T3)
S4 (S3 + axiom M9, or M + axiom 4)
S5 (M + axiom 5, or S4 (from M) + axiom B, or S4 (from S3) + axiom B, or S1⁰ + axiom M10)
V1 (S4 + axiom M24)
V2 (S5 + axiom M24)

The Challenge

Develop a computer program that, when given the bases of two logics or two axiomatizations of one logic (from the lattice above), determines the relationship between the two.

The program cannot simply encode the known relationships shown; it must use logical reasoning from the bases to establish the relationship (as would be the case if the relationship were unknown).
The program may not store any precomputed information about the logics. The relationship must be determined from only the input bases.
The syntactic representation of the axioms and rules can be anything reasonable (use of the TPTP syntax is encouraged).

This is an annual challenge, with the most successful program each year receiving "a bright shiny $100 bill". The award will be made at the CADE (or IJCAR) conference each year. Programs must be made available to the organizers one month in advance of the conference in order to be eligible. The next award will be made at CADE-21.

The winners of the 2005/2006 challenge were (independently) Florian Rabe and Weina Shen. The winner of the 2007 challenge was Petr Pudlak.

The $100 challenge is organized by Geoff Sutcliffe. All questions should be emailed to the organizer.