Entrants' System Descriptions

• Drodi 4.1.0
• iProver 3.9
• LastButNotLeast 0
• Prover9 1109a
• Vampire 4.4
• Vampire 4.9
• Zipperposition 2.1.9999

• Ordered resolution and equality paramodulation inferences as well as demodulation and some other standard simplifications.
• A basic implementation of clausal normal form conversion as in [NW01].
• AVATAR architecture with a SAT solver [Vor14].
• Limited Resource Strategy [RV03].
• Discrimination trees.
• KBO, non recursive and lexicographic reduction orderings. KBO has been rewriten using the polynomial-time algorithm in [BS23].
• Literal selection including lookahead as in [HR+16].
• SInE distance for clauses and symbols as in [Sud19].
• Layered clause selection as in [GS20].
• Stochastic strategy inspired in [Sud22].
• Drodi produces a (hopefully) verifiable proof in TPTP format.

Strategies

• Otter, Discount and Limited Resource Strategy [RV03] saturation algorithms.
• A basic implementation of AVATAR architecture [Vor14].
• Several literal and term reduction orderings.
• Several literal selection options [HR+16].
• Several layered clause selection heuristics with adjustable selection ratios [GS20].
• Classical clause relevancy pruning.
• Drodi V4 has new strategy portfolio inspired (but not exactly equal than) by [BS23]. The strategies have now unequal time slices and the set of strategies used depends on the problem features detected during the preprocessing.
• Some strategies are run a second time with a previously applied randomization to the problem [Sud22].
• Drodi can generate learning data from successful proofs and use the data to guide clause selection strategy. It is based in the enhanced ENIGMA method. However, unlike ENIGMA, the learning data is completely general and can be used with any kind of problems. This generality allows the use of the same learning data in both FOF and UEQ CASC competition divisions. The learning data is generated over a set of TPTP problems before the CASC competition using built-in Drodi functions that include a L2 Support Vector Machine. Drodi integrated learning functions are a generalization of ENIGMA [JU17, JU18]. Literals polarity, equality, skolem and variable occurrences are stored in clause feature vectors. Unlike ENIGMA, instead of storing the specific functions and predicates themselves only the SinE distance and arity of functions and non equality predicates are stored in clause feature vectors with different features assigned to predicates and functions.

Implementation

Expected Competition Performance

Recent features in iProver include:

• Ground joinability and connectedness in the superposition calculus [DK22].
• Support for quantified reasoning with arithmetic and arrays.
• AC joinability and AC normalisation [DK21].
• Superposition calculus with simplifications including: demodulation, light normalisation, subsumption, subsumption resolution and global subsumption. iProver's simplification set up [DK20] is tunable via command line options and generalises common architectures such as Discount or Otter.
• HOS-ML framework for learning heuristics using combination of hyper-parameter optimisation and dynamic clustering together with schedule optimisation using constraint solving [HK21, HK19]

Strategies

Implementation

    https://gitlab.com/korovin/iprover

Expected Competition Performance

#!/usr/bin/env python

print("% LastButNotLeast: The fastest way to give up!")
print("% For best results, do not expect results.")
print("% SZS status GaveUp")
print("% It's not a bug - it's a philosophical stance.")
print("% Thanks for trying LastButNotLeast :)")

Prover9 has available positive ordered (and nonordered) resolution and paramodulation, negative ordered (and nonordered) resolution, factoring, positive and negative hyperresolution, UR-resolution, and demodulation (term rewriting). Terms can be ordered with LPO, RPO, or KBO. Selection of the "given clause" is by an age-weight ratio.

Proofs can be given at two levels of detail: (1) standard, in which each line of the proof is a stored clause with detailed justification, and (2) expanded, with a separate line for each operation. When FOF problems are input, proof of transformation to clauses is not given.

Completeness is not guaranteed, so termination does not indicate satisfiability.

Strategies

Given a problem, Prover9 adjusts its inference rules and strategy according to syntactic properties of the input clauses such as the presence of equality and non-Horn clauses. Prover9 also does some preprocessing, for example, to eliminate predicates.

For CASC Prover9 uses KBO to order terms for demodulation and for the inference rules, with a simple rule for determining symbol precedence.

For the FOF problems, a preprocessing step attempts to reduce the problem to independent subproblems by a miniscope transformation; if the problem reduction succeeds, each subproblem is clausified and given to the ordinary search procedure; if the problem reduction fails, the original problem is clausified and given to the search procedure.

Implementation

    http://www.cs.unm.edu/~mccune/prover9/

Expected Competition Performance

A number of standard redundancy criteria and simplification techniques are used for pruning the search space: subsumption, tautology deletion, subsumption resolution and rewriting by ordered unit equalities. The reduction ordering is the Knuth-Bendix Ordering. Substitution tree and code tree indexes are used to implement all major operations on sets of terms, literals and clauses. Internally, Vampire works only with clausal normal form. Problems in the full first-order logic syntax are clausified during preprocessing. Vampire implements many useful preprocessing transformations including the SinE axiom selection algorithm.

When a theorem is proved, the system produces a verifiable proof, which validates both the clausification phase and the refutation of the CNF. Vampire 4.4 provides a very large number of options for strategy selection. The most important ones are:

• Choices of saturation algorithm:
  • Limited Resource Strategy [RV03]
  • DISCOUNT loop
  • Otter loop
  • Instantiation using the Inst-Gen calculus
  • MACE-style finite model building with sort inference
• Splitting via AVATAR [Vor14]
• A variety of optional simplifications.
• Parameterized reduction orderings.
• A number of built-in literal selection functions and different modes of comparing literals [HR+16].
• Age-weight ratio that specifies how strongly lighter clauses are preferred for inference selection.
• Set-of-support strategy.
• For theory-reasoning:
  • Ground equational reasoning via congruence closure.
  • Addition of theory axioms and evaluation of interpreted functions.
  • Use of Z3 with AVATAR to restrict search to ground-theory-consistent splitting branches [RB+16].
  • Specialised theory instantiation and unification [RSV18].
  • Extensionality resolution with detection of extensionality axioms
• For higher-order problems:
  • Translation to applicative and combinator form.
  • Addition of combinator axioms.
  • Addition of shortcut inference rules that encode axioms.
  • Proof search heuristics targetting the growth of combinator axioms.
  • Restricted combinatory unification [RSV18].

Implementation

Expected Competition Performance

Strategies

• Choices of saturation algorithm:
  • Limited Resource Strategy [RV03]
  • DISCOUNT loop
  • Otter loop
  • MACE-style finite model building with sort inference
• Splitting via AVATAR [Vor14]
• A variety of optional simplifications.
• Parameterized reduction orderings.
• A number of built-in literal selection functions and different modes of comparing literals [HR+16].
• Age-weight ratio that specifies how strongly lighter clauses are preferred for inference selection. This has been extended with a layered clause selection approach [GS20].
• Set-of-support strategy with extensions for theory reasoning.
• For theory-reasoning:
  • Ground equational reasoning via congruence closure.
  • Addition of theory axioms and evaluation of interpreted functions [RSV21].
  • Use of Z3 with AVATAR to restrict search to ground-theory-consistent splitting branches [RB+16].
  • Specialised theory instantiation and unification [RSV18].
  • Extensionality resolution with detection of extensionality axioms

Implementation

Expected Competition Performance

Strategies

Implementation

Zipperposition's code can be found at

    https://github.com/sneeuwballen/zipperposition

Zipperposition can also output graphic proofs using graphviz. Some tools to perform type inference and clausification for typed formulas are also provided, as well as a separate library for dealing with terms and formulas [Cru15].

Expected Competition Performance