Leo II live!

This the online version of LEO II. Define a problem in the textarea below and check if LEO II can prove it.

The Problem

Define the problem you want to prove here:


Example Problems

Choose one of the examples below:

Fitting-HB-1.thfFitting-HB-10.thfFitting-HB-11.thf
Fitting-HB-11b.thfFitting-HB-12.thfFitting-HB-13.thf
Fitting-HB-14.thfFitting-HB-15.thfFitting-HB-2.thf
Fitting-HB-3.thfFitting-HB-4.thfFitting-HB-5.thf
Fitting-HB-6-KB.thfFitting-HB-6-T.thfFitting-HB-7a.thf
Fitting-HB-7b.thfFitting-HB-8.thfFitting-HB-9.thf
Fitting-HB-Knowledge-1.thfFitting-HB-Knowledge-1b.thfFitting-HB-Knowledge-2.thf
Fitting-HB-Knowledge-2a.thfFitting-HB-Knowledge-2b.thfFitting-HB-Knowledge-3b.thf
Fitting-HOLML-Ex-God-alternative-a.thfFitting-HOLML-Ex-God-alternative-b.thfFitting-HOLML-Ex-God.thf
K-4-b.thfK-4-e.thfK-4-f.thf
K-D.thfK-N.thfK-T-b.thf
K-T-c.thfK-T4-a.thfK-T4-b.thf
K-T4-c.thfK-T4-f.thfK-a.thf
K-b.thfK-d.thfK-e.thf
K-f.thfK-g.thfK-h.thf
K-i.thfK-j.thfK-k.thf
NL_2.thfNL_3.thfNL_4.thf
NL_5.thfNL_6.thfNL_7.thf
NL_8.thfSET014+4.thfSET017+1.thf
SET066+1.thfSET067+1.thfSET076+1.thf
SET086+1.thfSET096+1.thfSET143+3.thf
SET171+3.thfSET580+3.thfSET601+3.thf
SET606+3.thfSET607+3.thfSET609+3.thf
SET611+3.thfSET612+3.thfSET614+3.thf
SET615+3.thfSET623+3.thfSET624+3.thf
SET630+3.thfSET640+3.thfSET646+3.thf
SET647+3.thfSET648+3.thfSET649+3.thf
SET651+3.thfSET657+3.thfSET669+3.thf
SET670+3.thfSET671+3.thfSET672+3.thf
SET673+3.thfSET680+3.thfSET683+3.thf
SET684+3.thfSET716+4.thfSET724+4.thf
SET741+4.thfSET747+4.thfSET752+4.thf
SET753+4.thfSET764+4.thfeshol08-1a.thf
eshol08-1b.thfeshol08-2a.thfeshol08-2b.thf
eshol08-2c.thfeshol08-3.thfijcar08-ex1.thf
ijcar08-ex2.thfijcar08-ex3.thf

Futher Examples

Further examples (by C. Brown) can be found here:

Properties of an Explicit Substitution M-set Model
Basil Smith's Elementary Theory of Relations

You can either call LEO II on these problems or prove them interactively in C. Brown's interactive javascript tableaux prover JITPRO.