                    THE LEO-II System -- Changes

v1.9.4
------

1.9.4 proves more than 1.8.0 within the same time limit.  The calculus is
untouched: not one inference was added, removed or changed.  What changed is
how the time budget is divided, how much work is done and thrown away, and --
with --cores, which is what the fourth digit of this version number is about --
whether the settings that disagree with each other run one after another or
side by side.

The gain is a net one.  A handful of problems that 1.8.0 proves are lost, as
always when a search order changes; the figures below are the balance.

Three errors in the arithmetic of time

  * The number of time slices was not bound by what the budget can carry.  At a
    ten-second limit the budget was cut into four slices of two and a half
    seconds, and in each of them one call to the first-order prover was
    scheduled with a floor of three seconds.  The first call overran its slice,
    and the strategies after it never ran.  The slice count is now capped by
    the time a slice must be able to hold.
  * The local time limit was derived from the configured slice count while the
    scheduler created a different number of slices, so the prover was given a
    limit computed for slices that did not exist.  Both now use the same
    number.  The sources carried a FIXME asking exactly this question.
  * One call to the first-order prover could take half of its slice, and the
    first was made only at the tenth iteration of the main loop.  Both come
    from a time when such a call was expensive.  A call now takes at most a
    fifth of its slice and is made at every iteration.

Work that was thrown away

  * The message passed to sysout was built at every call site whether or not it
    would be shown, and at the default verbosity none of it is.  363 call sites
    pass a thunk now.  The clause renderings in the innermost loops were the
    dominant cost: the unification search built one at every node.
  * Six deep copies of the clause sets per iteration of the main loop, into two
    fields that nothing reads, are gone.
  * Assembling the translated first-order problem was quadratic in its size, on
    every call to the first-order prover, and the guard against duplicate
    clause names was quadratic in their number.
  * The native build no longer passes -inline 0.

Reading more of TPTP

  * A single-quoted atom is a legal type name.  69 THF problems of the library
    use one and could not be read at all.

A parallel portfolio, off by default

  * --cores N runs N branches at once and answers with the first that settles
    the problem.  A branch is this same binary re-executed with different
    flags, so each takes the ordinary code path and the soundness of the whole
    is the soundness of one run; nothing is shared between branches but the
    answer.  The branches are listed at portfolio_branches in src/toplevel/leo.ml.
  * The reason to run them side by side rather than one after another is that
    the settings which solve what the default cannot are the same settings that
    lose most of what it can.  The relevance filter is the plain case: on its
    own it answers 96 of 294 where the default answers 167, and it answers 20
    of the 126 the default misses.  Measuring it only on those 126 makes it
    look like the best lever there is, which is how it was nearly made a
    default.  A setting like that is worthless first and valuable second.
  * The default is one core, at which none of this code runs.  That keeps the
    prover comparable with the single-core first-order provers it is usually
    measured against, and makes the parallel figures below a statement about
    what four cores buy, not a like-for-like comparison with them.
  * A branch stays in the process group it was forked in.  Giving each its own
    session, so that killing a branch would also kill the first-order prover
    under it, was tried and is wrong: a signal to the process group is how
    callers stop this prover, and a branch outside the group survives it.  Over
    294 problems that left four immortal branches behind for every problem that
    ran out of time.  A first-order prover left behind by a killed branch stops
    on its own CPU limit instead.

Costs that grew with what had already been proved

  * A term is stored as an index and an int, and two terms in one index are
    equal exactly when the ints are.  The hot paths compared them with the
    structural "=", which walks the whole term base before reaching the ints,
    and walks it in full even when the terms plainly differ.  Every comparison
    therefore cost the size of everything proved so far.  literal.mli already
    declared lit_term_equal for this and literal.ml defined it as a failure,
    so the call sites used "=" instead; it is implemented now and used in the
    three places sampling found: Termsystem.get_id, subsumption, and the first
    guard of the pre-unification match, which runs once per unification
    literal per step of the recursion.
  * Primitive substitution built all four levels of bindings and then read the
    flag deciding which to return, so "--primsubst 0" produced an empty list at
    full price.  Each level is a function now.  The costly one walks the whole
    signature, which grows with every Skolem constant.
  * Every fresh variable and every Skolem constant refolded the entire
    signature into a new list to keep a table that only the term orders read,
    and the default order reads nothing.  One new symbol adds one entry now.

These change what the prover spends, never what it answers.

Problems LEO-II could not read at all

  * "~ ? [X] : F" and "~ ! [X] : F".  The grammar took "~ (F)" and, since
    1.8.0, "~ P", but not a negated quantification, which is ordinary THF and
    which the library is full of.
  * "~ ~ F".  Its own production, because "~" is itself an atom and "~ ~" was
    taken by the rule above.
  * A base type declared twice.  TPTP problems restate the types of the axiom
    files they include; LEO-II refused them.  A base type is its name and
    nothing else, so the second declaration says what the first said.
  * A type printed as a variable.  type_to_term encoded a polymorphic type as
    a bare capital letter, which in a first-order problem is a variable, and
    the first-order prover rejected the whole problem with "Formula has free
    variables" -- silently, the call spent and its answer lost.  LEO-II's own
    "!=" carries such a type, which is why the primitive substitution levels
    that offer it never worked.
  * SIGPIPE.  A first-order prover that rejects its input exits at once, and
    the write still in flight killed LEO-II outright: no status, no exit code
    of its own, a prover that vanished rather than failed.

Of 584 TH0 problems sampled evenly across TPTP, 197 ended in an error rather
than an answer.  None do now, and 70 of them are proved.

Measured over those 584, at ten seconds and on one core:

    1.9.4 before these fixes   278
    1.9.4                      348

The 584 are the TH0 problems among 800 drawn evenly from the TPTP THF
theorems.  The other 216 are TH1 and the fragments beside it, which LEO-II is
not for and says so at once; counting them would measure the sampling rather
than the prover.  test/tptp_check.py --th0 selects the TH0 problems.

Measured over the 294 higher-order problems of Benzmueller and Scott's
ontological-argument dataset, against 1.8.0 under identical conditions:

    limit     1.8.0    1.9.4    1.9.4 --cores 4
    10 s       154      175          197
    60 s       171      186          210

The four-core figures are what four cores buy; E, Vampire and Leo-III are
measured on one core, so the one-core column is what compares with them.

Repeated runs of the same build differ by about two problems.  For scale, on
the same problems and the same limit of ten seconds, Vampire proves 173,
Leo-III 158, and E 209.

None of the 45 statements the dataset records as non-theorems is proved at
either limit, by either version, on one core or on four.

Over 477 TPTP THF problems recorded as having a countermodel, 1.9.4 claims a
proof of none of them, on one core or on four.  test/tptp_check.py runs that
check, and --leoargs puts a candidate setting through it before it becomes a
default.  It is not decoration: the fof_experiment_erased translation proves
170 of the 294, six more than the default encoding, and proves four TPTP
problems that have countermodels.  Erasing types buys those six with
unsoundness, and LEO-II does not reconstruct the first-order proofs that would
catch it.  The default encoding is unchanged.

v1.8.0
------


LEO-II 1.8.0 proves what 1.7.0 proves.  Every change below is either a
portability fix or something switched off by default.  The point of the release
is that the prover builds and runs on a current system again.

Building

  * No preprocessor.  camlp4 has no OCaml 5 release, so the macros it provided
    are gone.  What they decided now lives in src/general/build_config.ml, a
    file the Makefile writes from the same variables that used to become -D
    switches, and the sites that used IFDEF are ordinary conditionals.  The
    build needs no package beyond ocamlfind.
  * OCaml 5.  Tested with 5.5.0 and OTP 29, and still builds on OCaml 4.02 and
    later.  Two constructs only camlp4 accepted are written in standard OCaml,
    the removed String.uppercase family and Pervasives are replaced, and the
    compiler is told where unix and str live under the 5.0 library layout.
  * C++11 and later.  The bundled MiniSAT separated its PRI* macros from the
    adjacent string literals, and the default argument in the mkLit friend
    declaration moved to the definition.  No -std fallback is needed.
  * The build is warning-free.

Behaviour

  * E is called with --auto.  LEO-II passed -xAuto -tAuto, whose values E 3.x no
    longer accepts, so every call to its first-order partner failed silently and
    LEO-II was left with its own calculus.  That was not merely a loss of yield:
    saturating with an incomplete calculus, it could report CounterSatisfiable
    for a statement that is a theorem.
  * The THF parser reads an unparenthesised negation.  The grammar accepted only
    ~ (F), so the standard ~ P failed with a syntax error.

New, and off by default

  * A term order, in src/datastructure/ncpo.ml: the computability path order of
    Niederhauser and Middeldorp, adapted to LEO-II's terms.  It is not known to
    be transitive, so it decides one pair at a time and must never be used to
    sort; see ncpo.mli.  "make ncpo_test" checks it against the worked examples
    of the paper.  Nothing in the calculus calls it yet.
  * A clause weight and a given-clause selection that alternates between the
    lightest and the oldest clause, in the ratio --ageWeightRatio sets.  Select
    it with --order weight.  Over the 294 higher-order problems of Benzmueller
    and Scott's ontological-argument dataset it proves as many as the default
    does and no more, which is why it is not the default.

Fixed along the way

  * Term.compare compared term weights, so two distinct terms of equal weight
    compared equal and a set keyed on it dropped elements silently.
  * The weight behind the "naive" setting sorted the whole signature on every
    symbol lookup.
  * Six handlers matched the message inside a Failure value; they raise and
    catch named exceptions now, continuing what the sources had begun.

v1.7.0 and earlier
------------------

See the repository history at https://github.com/leoprover/LEO-II.
