                    THE LEO-II System -- Changes

v2.1
----

2.1 answers 217 of the 294 problems of the ontological-argument dataset at ten
seconds on one core, against 205 for 2.0; 0 of 45 non-theorems.  One change in
the schedule, one feature, two repairs.

**A short filtered slice first.**  The relevance filter (--relevancefilter 1,
axioms kept by shared symbols with the conjecture) had been measured as the
single largest lever on the problems the default misses, and as a loss as a
default: it drops axioms that a proof needs.  It is now the first of the two
time slices, with a quarter of the budget, for problems with long definitions
(the branch the ontological-argument problems take); the unfiltered search
gets the rest, and whatever the filtered slice leaves unused.  Measured, one
core, ten seconds: filter in the second of two equal slices 213, in the first
207, first with a quarter of the budget 217, last with a quarter 211.  What
the filter finds it finds in 0.1 to 1.1 seconds -- all five Ax2a_prime, six
UniqueEss3 -- and what it does not find fast it does not find at all.  The
slice lengths are computed in leo.ml, the strategy is in
strategy_scheduling.ml with the measurements beside it.  On a sample of 400
TH0 theorems across the TPTP the slice is neutral, 247 either way; on the 470
TPTP non-theorems and the 45 of the dataset nothing is proved.

**Questions are answered.**  A formula of role "question" is proved like a
conjecture, and the instances of its existential variables are reported:

    thf(q, question, (? [X: $i]: (p @ X))).
    % SZS status Theorem ...
    % SZS answers Tuple [[a]]

The answer comes from the first-order prover.  LEO-II negates and clausifies the
question as it does a conjecture; the clauses that descend from it and still
carry free variables are what an answer must instantiate, and handed to E as
axioms they would let it refute the problem without saying which instance did
it.  They are bundled instead into one formula of role "question",
?[X1..Xn]: (~C1 | ... | ~Ck) -- the negation of the conjunction of the
universally closed clauses, hence equivalent -- and E is run with --answers=1.
Its answer is a term over LEO-II's own first-order encoding and is read back
out of it: type tags dropped, applications written with @, the constant prefix
removed, a lambda-lifted symbol replaced by the term it stands for.  Two things
to know.  The answer is given after definition unfolding, so a defined symbol
appears as its definiens; and a variable the prover left uninstantiated is
printed as it came (X1), which for a disjunctive question is the right answer.
E reports Theorem for a problem with a question where it reports Unsatisfiable
for a clause set; both count as success now.  Explicit $answer literals in the
clauses would have been simpler, but E ignores them in cnf and fof input.

**"--proofoutput 2" finds epclextract by itself.**  It expands the first-order
steps of a proof with epclextract, which ships with E and lives next to
eprover; when .leoatprc does not name it, LEO-II now looks there.

The debug print "Hallo: type of symbol X unknown" that directory mode showed on
every problem is a warning on verbosity level 1, worded as one.

The equality-of-literal-terms test in simplify compares indexed terms by
identifier instead of rebuilding them; neutral in the measurement, a cleanup.

v2.0
----

2.0 answers 205 of the 294 problems of the ontological-argument dataset at ten
seconds on one core, against 174 for 1.9.6, and 224 given the whole machine.
Neither figure is exact -- runs of the same binary vary by two or three, which
is the spread a ten second limit has on a machine doing anything else.  Four
things account for it, and none of them is in the calculus.

**When the first-order prover is called.**  After every iteration of the main
loop, which is what LEO-II had always done.  Each call costs the whole second
a time slice allows it, so ten calls exhaust a ten second limit; on QUA006^1
the main loop then ran *no* iterations at all -- ten calls, nothing proved --
and every one of those calls answered GaveUp, which is E saying it saturated:
the clauses a refutation needs had not been derived, because deriving them is
what the calls were preventing.  The partner was starving the search whose
results it needed.  Every fifth iteration instead: 205 against 180 here, and
332 of 400 small TH0 theorems drawn across the TPTP against 326.  This was the
largest single change, and it was found by looking for small problems that
another prover proves in under a second and LEO-II does not.

**The type tags handed to that prover.**  LEO-II encodes a higher-order problem
in first-order logic by tagging every subterm with its type, and a type was
itself a term: "mu > mu > $o" arrived as "leoFt(tmu, leoFt(tmu, o))".  On the
modal embeddings in this dataset those tags were the bulk of what E received --
a single atom came to 150 characters, most of it type.  A ground function type
is now one constant.  It is the same encoding up to a bijective renaming of
ground types, so it neither adds nor removes a refutation; what it removes is
weight, which a first-order prover carries through every ordering comparison
and every index lookup.  Worth about six problems.

Writing the tag itself as one symbol per type -- "leoTi_tfun22(cr)" rather
than "leoTi(cr, tfun22)" -- was implemented too, and measured, and is worse:
171 against 183 at the time.  Turning one frequent function symbol into thirty
rare ones costs more than the third of the length it saves.  There is a note
in translation_printing.ml saying so.

**The portfolio.**  "--cores" defaults to one, as E's "--auto-schedule" and
Vampire's "--cores" do, and 0 takes the machine.  The branches are a greedy
cover measured over all 294 problems, which is not the same as a cover
measured over the ones the default misses: on that subset "-rf 1 -ns" looks
like the second-best branch there is, and over all 294 it answers 106, because
it throws away more than it gains.  Four branches and not six, since a branch
runs a first-order prover beside itself and the fifth and sixth cost more in
contention than they add.

**A scratch directory per process.**  Every scratch name was built from the
problem's basename, so two LEO-IIs running at once on two problems that share
a basename wrote, and then unlinked, the same file.  The TPTP is full of
repeated basenames and so is any dataset of variants: measured on two such
problems run concurrently, twenty failures in thirty runs before, none after.
It had been showing up as one SZS status Error per few hundred problems,
always on whichever problem was running when the collision happened and never
reproducible on that problem alone.

Three exceptions that were being swallowed.  LEO-II reports CounterSatisfiable
when its clause set saturates, which is an argument only if the calculus that
produced it is complete; "-nux", "--primsubst 0" and the new "--defsasrules"
take rules away and were not in the list of settings that suppress the claim,
and "--defsasrules" duly claimed a countermodel for TestsHOMLinS4/EqPrimLeib,
a recorded theorem.  apply_subst caught everything and raised a bare Failure
in its place, including the exception that means the time is up, so a problem
whose clock ran out inside a substitution was answered Error rather than
Timeout.  And a clause the translation cannot render is now dropped rather
than taking the proof attempt with it -- giving the first-order prover fewer
clauses can cost a refutation it might have found and can never add one.

Two repairs in the translation itself, both reached only once a definition is
left folded: "!=" was descended into as though it were a connective, and its
arguments are terms, not formulas; and the quantifier recognition knew "!" but
never "?", so an existential inside a term was lifted and then typed wrong.

New options, none of them a default: "--atpmaxclauses N" bounds how many
clauses one call to the first-order prover is given, lowest weight first;
"--defsasrules" keeps definitions folded and gives the search "d = body" as an
axiom instead; "--instantiate N" also instantiates a universal variable with
the problem's own lambda abstractions.  Each is worth a few problems in the
right place and loses more than it wins as a default; the figures are in the
comments on the flags.

For scale, on the same 294 problems at the same limit: E 3.2 answers 209 with
"--auto", 218 with its own schedule on one core and 227 with that schedule on
six; Vampire 4.8 answers 174; Leo-III answers 160.

Soundness, TPTP v9.2.1, TH0 only: 470 non-theorems on one core and again with
the portfolio, 0 proved and no contradiction against the record either time;
400 theorems sampled across the library, 259 proved, no countermodel claimed
for any of them.

v1.9.6
------

1.9.6 makes "-t" a limit on the run.  In 1.9.5 it bounded a time slice, and
the work that happens outside a slice was unbounded: on 106 of 584 TH0
problems drawn from TPTP the prover ran more than sixteen seconds at "-t 10",
and on some it did not stop at all.  Six do now, and the worst case fell from
over two minutes to fifteen seconds.

  * The clock is read while a clause is indexed.  The position of a subterm is
    a list, one element per step into the term, and it is the key of a
    hashtable, so comparing keys costs their length; on a problem with deep
    terms that was 98% of the run, inside a single call that nothing
    interrupted.
  * The clock starts when the prover does, not when the first slice is made.
    Reading the problem and choosing the strategies happens before any slice
    exists and can outlast the whole limit.
  * A repeating real-time alarm backs both up.  It arrives wherever the prover
    happens to be, so a loop does not have to know about the limit to respect
    it.  It repeats because a single alarm is swallowed by any handler that
    catches everything.

Also, two kinds of work that nothing reads: every clause was rendered into a
string for a proof protocol that is only kept when proof output was asked for,
and 208 debug calls built their strings before the verbosity was tested -- one
at level 0, so a whole clause was printed for every application of primitive
substitution.

What the prover proves is unchanged: 175 of the 294 problems of the
ontological-argument dataset and 345 of the 584, both within the spread of the
1.9.5 figures.  0 of 45 non-theorems, and no contradiction against the record
on the 477 TPTP problems with countermodels.

v1.9.5
------

1.9.5 is 1.9.4 with three repairs and no change to what the prover proves.

  * LEO-II no longer waits for a first-order prover that never answers.  It
    read that prover's output to end of file, and it checks its own clock only
    between inference steps, so a partner which never closes its output stopped
    the prover dead: "-t 10" then ended the run neither at ten seconds nor at
    all.  An eprover-ho that does not take the --cpu-limit LEO-II passes does
    exactly that.  The call now has a deadline of its own -- the limit given to
    the prover plus five seconds for it to stop by itself -- and the prover is
    killed when that passes.  A prover that honours its limit never reaches it.
  * "--proofoutput 2" no longer runs a command that is not there.  It expands
    the first-order steps with epclextract, and with no epclextract entry in
    .leoatprc it handed the shell a command line beginning with a space, so the
    shell reported "--tstp-out: command not found" into the middle of the proof.
    It says what is missing instead.
  * Two costs in the term index: the name of a bound variable, which depends on
    its de Bruijn depth alone, was rebuilt on every retrieval, and the position
    of a subterm, which is a list and is the key of a hashtable, was hashed
    three times per subterm instead of once.

Measured at ten seconds on one core: 174 of the 294 problems of the
ontological-argument dataset, and 343 to 344 of 584 TH0 problems sampled from
TPTP.  Both are the figures of 1.9.4 within the spread of the measurement,
which is about two problems on the first set and at least three on the second;
these repairs are not meant to prove more, and they do not prove less.  0 of
45 non-theorems, and no contradiction against the record on the 477 TPTP
problems with countermodels.

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                      343-348

Five runs of that sample over these builds gave 348, 343, 344, 343 and 344, so
its spread is at least three and a single run of it settles nothing smaller.

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.
