# Using Counterexample Generation and Theory Exploration to Suggest Missing
Hypotheses

Ruben Gamboa This work was supported by a grant from the Defense Advanced
Research Projects Agency (DARPA) Proof Engineering, Adaptation, Repair, and
Learning for Software (PEARLS) Artificial Intelligence Exploration (AIE)
OpportunityUniversity of Wyoming
& Kestrel Institute
Laramie, Wyoming<EMAIL_ADDRESS>Northeastern University
Boston, MassachusettsKestrel Institute11footnotemark: 1
Palo Alto, CaliforniaUniversity of California San Diego
& Kestrel Institute11footnotemark: 1
San Diego, California Panagiotis Manolios Northeastern University
Boston, Massachusetts<EMAIL_ADDRESS>Kestrel
Institute11footnotemark: 1
Palo Alto, CaliforniaUniversity of California San Diego
& Kestrel Institute11footnotemark: 1
San Diego, California Eric Smith Kestrel Institute11footnotemark: 1
Palo Alto, California<EMAIL_ADDRESS>University of California San
Diego
& Kestrel Institute11footnotemark: 1
San Diego, California Kyle Thompson University of California San Diego
& Kestrel Institute11footnotemark: 1
San Diego, California<EMAIL_ADDRESS>
###### Abstract

Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they
believe should be theorems, such as (reverse (reverse x)) = x. Experienced
ACL2 users will recognize that the theorem only holds for intended values of
x, and given ACL2’s total logic, there are many counterexamples for which this
formula is simply not true. Counterexample generation (cgen) is a technique
that helps by giving the user a number of counterexamples (and also witnesses)
to the formula, e.g., letting the user know that the intended theorem is false
when x is equal to 10. In this paper we describe a tool called DrLA that goes
further by suggesting additional hypotheses that will make the theorem true.
In this case, for example, DrLA may suggest that x needs to be either a true-
list or a string. The suggestions are discovered using the ideas of theory
exploration and subsumption from automated theorem proving.

##  1 Introduction

Over the past year, the Kestrel PEARLS team has been working to implement
ideas to use machine learning tools to improve the experience of users in the
construction and repair of proofs. Most of these ideas revolve around The
Method [2]. In particular, we built an “advice” tool that can read an ACL2
checkpoint from a failed proof attempt, and suggest a number of routes the
user may take to resolve the issue. The advice is created from a variety of
models trained using machine learning techniques, as well as some heuristics
that would be familiar to ACL2 users. The models are trained by taking data
from the ACL2 Community Books, deliberating breaking the theorems in those
books, and submitting the broken theorem to ACL2. The model is trained to
recognize the checkpoint that ACL2 discovers when trying to prove the broken
theorem, and then suggest the fix that corresponds to the way the theorem was
originally broken. For example, one way to break a theorem is to remove an
include-book, so the proposed fix is to include that particular library book.

There are, of course, various ways to break theorems, thus various different
solutions that the advice tool may suggest. Besides removing library books, we
may remove hints, or remove hypotheses from the theorem itself. Two lessons we
learned while doing this are that (1) sometimes the advice tool could produce
valuable advice using only hardcoded suggestions instead of full-blown machine
learning (e.g., “try enabling all definitions”), and (2) advising the user to
add a hypothesis is inherently riskier than suggesting including a book or
adding a hint. The second point is simply unavoidable, since adding a
hypothesis _changes_ the logical meaning of the intended theorem. For
instance, suggesting the hypothesis NIL will result in a successful proof
attempt of a useless theorem. But a less blatant problem would be suggesting
the new hypothesis x <= 0 in a theorem that already has the hypothesis x >= 0;
the new theorem, which applies only to the case x = 0 may be easier to prove,
but it is also much less useful.

In light of this, and further considering the first point above, it is natural
to ask whether there are simple strategies—i.e., not based on machine learning
or artificial intelligence in general—that can be used effectively to suggest
missing hypotheses. This paper introduces DrLA, a tool that does precisely
this. Rather than use checkpoints from a failed proof attempt, DrLA infers
missing hypotheses by using the counterexample generation engine (cgen)
originally developed in ACL2s [5]. Cgen provides the user with both
counterexamples and witnesses to the proposed theorem, and DrLA uses theory
exploration techniques [4] to suggest the missing hypotheses. A key concept in
theory exploration is to consider only terms that do not reduce to terms that
have already been seen. In the context of generating hypotheses, this deals
effectively with the problem of suggesting hypotheses that trivialize the
original theorem.

The rest of the paper is organized as follows. Sect. 2 describes the necessary
background from theory exploration to then introduce the key ideas behind
hypothesis generation with DrLA. This is followed in Sect. 3 with a discussion
of the effectiveness of DrLA (and similar tools). Then Sect. 4 discusses some
details of the DrLA implementation. Finally, Sect. 5 provides some concluding
remarks and suggests avenues for the future evolution of DrLA and other tools
to ease proof development with ACL2.

##  2 Background and the Key Idea

Theory exploration is a technique for discovering likely properties of
programs or lemmas of a mathematical theory. For example, once the function
append over lists is defined, theory exploration may discover that append is,
in fact, associative. This is done by combining two tools: a formula generator
and a property checker (also known as a counterexample generator).

The formula generator creates formulas, i.e., possible theorems, from a given
set of function and constant symbols. In the case of list functions, it may
start with consp, nil, cons, car, cdr, append, and equal. Using this
vocabulary, the theory exploration tool may create some familiar theorems such
as

  * •

(equal (car (cons x1 x2)) x1)

  * •

(equal (append (append x1 x2) x3) (append x1 (append x2 x3)))

as well as reasonable-looking formulas that are not theorems, e.g.,

  * •

(equal (car (cons x1 x2)) x2)

  * •

(equal (append x1 x2) (append x2 x1))

and complete nonsense, such as

  * •

(consp (equal (car nil) (append x1 x2)))

  * •

(car (cons (cdr x1) (equal x2 nil)))

Theory exploration then considers each of these formulas in turn, and
determines which of them are likely to be true. This is where the property
checker comes in, by methodically searching for counterexamples to each
formula. E.g., the first conjecture is (equal (car (cons x1 x2)) x1), and it
has the variables x1 and x2, so the property checker will consider thousands
of random or strategically chosen values for them, such as x1=3, x2=’(1 2) or
x1=’(a . 16), x2=’bgs. In all cases, the formula ends up being true, so theory
exploration will suggest this formula as a _likely_ lemma. Theorem proving can
then be used to confirm that it is an _actual_ lemma, and some theory
exploration systems do this.

In the case of spurious theorems, theory exploration can often find an
assignment that demonstrates the formula cannot be true. E.g., the binding
x1=3, x2=’(1 2) from above suffices to show that the formula (equal (car (cons
x1 x2)) x2) cannot be true, so it would never be suggested as a likely lemma.
The same is true of the nonsensical formulas, though care must be taken with
respect to runtime errors, since these expressions may violate guards freely.

So the result of theory exploration is a list of theorems, or at least likely
conjectures. The goal is to produce enough formulas that the tool can find a
sufficient number of useful theorems. Obviously there is a delicate balance
involving the formula generator. Ideally, it should generate as many formulas
as possible, so that useful lemmas can be discovered. But the process of
generating random formulas grows exponentially with their length, so limits
are unavoidable, and efficient strategies are used to prune the space of
candidate formulas so that barren areas of the search space are not explored.
In practice, this means that the theorems discovered are usually small
syntactically, e.g., limited in terms of depth.

For our purposes, we are interested in discovering not likely lemmas, but
likely hypotheses that may be missing from a theorem. The overall strategy
remains the same: A term generator will produce candidate hypotheses, and a
property checker can determine if each possible hypothesis is likely to make
the theorem provable. But a key idea is that we can leverage the work of the
property checker since the hypotheses are always in the context of a
surrounding formula, as opposed to theory exploration where the generated
formulas are all at the top level. E.g., consider the motivating example
(equal (reverse (reverse x)) x). It is a reasonable heuristic to expect that
any missing hypothesis will feature only the variable x, so we can generate
values for x ahead of time and test all candidate hypotheses with the same set
of bindings.

In fact, we can do a bit better than that. Cgen, the counterexample generator
developed as part of ACL2s, is a sophisticated tool that will find both
counterexamples and witnesses to an ACL2 formula. For our motivating example,
cgen will identify the following counterexamples

  * •

((X ’((T . 1) NIL . #$\backslash$A)))

  * •

((X ’(-25 . 0)))

  * •

((X ’(53 . 252)))

and the following witnesses

  * •

((X ’((T T) (#$\backslash$A 1))))

  * •

((X NIL))

  * •

((X ’(-1)))

Readers experienced with ACL2 will immediately recognize that all of the
witnesses are true lists, whereas none of the counterexamples are—which
immediately suggests (true-listp x) as the missing hypothesis.

DrLA proceeds in a similar manner. The basic idea is to find an expression
that is false for all of the counterexamples and true for all witnesses111We
will see later that it is not necessary, or even desirable, for the property
to hold for all witnesses, but this is a good first approximation.. This
evokes the machine learning idea of finding a “hyperplane” that separates the
positive and negative examples in a training data set. This is straightforward
to do with a general property checker, as in theory exploration.

The more interesting component is the term generator. What should be the
language (i.e., function symbols) that determines the possible terms that lead
to possible hypotheses? It is often the case that the missing hypothesis is a
type hypothesis. ACL2 is an untyped language, but many functions are written
with specific types in mind. This is certainly the case where reverse is
concerned, since the obvious programmer intent is for reverse to work with
lists, more specifically true-lists. Theorems about these functions usually
require some typing hypothesis to make explicit the intended use of the
function, and such hypotheses are easy to miss.

The tau system is an important component of ACL2 that helps the theorem prover
benefit from the implicit notions of type assumed by programmers [3]. Tau is
designed “to be a lightweight, fast, and helpful decision procedure for an
elementary subset of the logic focused on monadic predicates and function
signatures” [3]. So a reasonable language for the term generator is the set of
types (“monadic predicates”) in use by the tau system. This set begins with a
hard-coded list of primitive predicates, including consp, natp, and so on. The
set is enhanced when new definitions are encountered, e.g., primep, but only
monadic predicates are considered. To account for the fact that sometimes the
result of comparisons is a useful notion of type, tau hardcodes some common
comparisons as primitive type predicates, e.g., 0 <= x, 1 < x, and “x is a
non-NIL true-listp.” DrLA adopts the primitive types recognized by the tau
system, but unlike the tau system, it does not currently expand this
dictionary as new functions are introduced. Rather, it uses the the predicates
mentioned in the theorem and used in the definitions of functions present in
the theorem. For example, when considering (equal (reverse (reverse x)) x), it
will add the function reverse to the list of types, as well as functions used
in its definition such as revappend. This illustrates another departure from
the tau system, in that revappend is a binary function, so it would be ignored
by the tau system.

DrLA will take these selected symbols and generate terms by nesting
syntactically valid function invocations. These terms are the expression trees
that can be generated using these function symbols up to a maximum depth. The
leaves of the terms correspond to either variable symbols, which must occur in
the original theorem, or one of a list of predefined constant symbols, e.g., 0
or NIL. Thus, DrLA will explore terms including the following:

  * •

(posp x)

  * •

(consp x)

  * •

(reverse x)

  * •

(revappend x 0)

  * •

(equal (reverse x) x)

DrLA will also consider boolean combinations of these terms, up to a maximum
depth. For example, DrLA may consider the hypothesis (or (posp x) (consp x)).
DrLA allows the user to control all of the depth parameters: how many levels
of function definitions to explore for new function names, how deeply to nest
boolean expressions, and how deeply to nest non-boolean terms such as (reverse
(reverse x)).

We will have more to say about the implementation of DrLA in Sect. 4, but it
is important to note now that DrLA attempts to avoid unnecessary computation
when exploring the search space. For instance, DrLA is aware that the boolean
predicates and and or are commutative, so it considers only one of the terms
(and P Q) or (and Q P). Moreover, it avoids nesting the primitive predicates,
so that it will consider (posp (reverse x)) but never (posp (consp x)).

As described thus far, DrLA will respond to the motivating example with an
excess of possible hypotheses. Included in this list is the expected (true-
listp x). But DrLA also finds other possible suggestions, such as

  * •

(equal x ’nil)

  * •

(equal (revappend x x) ’nil)

  * •

(true-listp (revappend x x))

  * •

(and (consp x) (true-listp x))

  * •

(and (true-listp x) (equal (reverse x) ’nil))

Actually, DrLA finds dozens of similar, unhelpful suggestions.

Thus, the final component of DrLA is a filter that reduces the number of
suggestions in a manner reminiscent of subsumption. Specifically, suppose that
DrLA has two suggestions $P$ and $Q$ such that $P\rightarrow Q$ but
$Q\not\rightarrow P$. For example, $P$ may be (natp x) while $Q$ is (integerp
x). We say in this case that $Q$ is more general (logically weaker) than $P$,
and we prefer to suggest $Q$. With this heuristic, DrLA will suggest (true-
listp x) but not (equal x ’nil) since (true-listp x) is the more general term.
This heuristic eliminates many of the useless suggestions above, but not all.
For instance, (true-listp (revappend x x)) is logically equivalent to (true-
listp x), so neither is more general than the other. In these cases, a
complexity heuristic comes into play—if $P$ and $Q$ are logically equivalent
and $Q$ is syntactically simpler than $P$, DrLA will suggest $Q$ but not $P$.
Our notion of syntactic complexity is simple and partial, so it is possible
that DrLA will find two suggestions that are logically equivalent and just as
simple syntactically. In these cases, DrLA will offer both suggestions,
letting the user pick which one to use as the “better” hypothesis.

As mentioned previously, this notion of “more general” is similar to the
notion of subsumption in resolution theorem proving. In the implementation of
DrLA, it is used in much the same way. First, a suggestion is ignored if it is
subsumed by a prior suggestion (c.f. forward subsumption.) Then, when a
suggestion is added to the list of suggestions, prior suggestions subsumed by
the new one are discarded (c.f. backward subsumption.)

We note briefly that these heuristics also have a useful side-effect. In Sect.
1, we warned about the dangers of suggesting vacuous hypotheses, such as nil.
In fact, DrLA would never make such a suggestion, since such hypotheses would
never be true of all the witnesses. But DrLA may suggest overly constrained
hypotheses, such as (equal x ’nil). However, the heuristics described will
rule out that hypothesis in favor of the more general (true-listp x).

With these heuristics, DrLA suggests a single hypothesis to the user, but it
is _not_ the expected (true-listp x). Instead, DrLA suggests that the correct
theorem is

        (implies (or (stringp x)
                     (true-listp x))
                 (equal (reverse (reverse x)) x))

We believe that most users of ACL2 think of reverse as a function that
operates on lists, but in fact the programmers of this function allowed for
both lists and _strings_. The heuristics of DrLA select this hypothesis since
it is more general than the expected (true-listp x).

##  3 Assessment

In this section we describe our efforts to assess the performance of DrLA. The
approach is to give DrLA versions of theorems from the Community Books, after
removing one or more of the hypotheses in the theorem. This is the same idea
used to assess the more general advice tool that we built as part of the
PEARLS project, but with an important difference. The other suggested fixes
address the proof itself, e.g., by suggesting a hint. DrLA, on the other hand,
suggests a modification to the theorem, e.g., a new hypothesis to add. DrLA is
never invoked unless cgen demonstrates that the theorem is false, i.e., by
finding some counterexamples.

What this means for assessment is that it is insufficient simply to check if
the the suggestion results in a successful proof attempt. What is really
important is to determine whether the suggestion matches the original intent
of the ACL2 user, who presumably forgot to list one of more key hypotheses.
Simply comparing the suggested hypothesis with the original one, i.e., the one
that was removed earlier, is also insufficient, because there may be more than
one way to express the necessary constraint.

So we chose to do much of the assessment manually, by running DrLA on examples
from the Community Books and determining whether DrLA’s output is effective.
For example, the book std/lists/append.lisp is part of the lists library in
ACL2, and it starts with the theorem

        (implies (consp x)
                 (< 0 (len x)))

Removing the hypothesis leaves just (< 0 (len x)), and when this is submitted
to DrLA, it provides a single suggestion: (consp x). Moreover, DrLA reports
that after adding this hypothesis to the theorem, ACL2 is indeed able to find
a proof. In this specific example, DrLA’s performance is an unqualified
success.

The next theorem in the file is

        (implies (not (consp x))
                 (equal (append x y)
                        y))

When DrLA is prompted with the conclusion, it suggests (atom x) as the missing
hypothesis. Note that atom is defined in ACL2 as not consp, so this is 100%
consistent with the original theorem, although not identical. This is why we
think a manual assessment process is necessary.

A more interesting theorem is

        (iff (append x y)
             (or (consp x)
                 (consp y)))

DrLA does not support iff, but we can use this by breaking the theorem up into
two implications. When presented with (append x y), DrLA accurately suggests
(or (consp x) (consp y)), but it also makes a number of other suggestions
which, while valid, are less useful. For instance, it suggests (or
(acl2-numberp y) (consp x)). Notice that neither of these suggestions subsumes
the other, and neither is syntactically simpler than the other, so DrLA
suggests both222Actually, DrLA gives six total suggestions in this case. and
lets the user decide which is the best alternative.

In the other direction, DrLA is completely ineffective. There are many
witnesses and counterexamples for (or (consp x) (consp y)), but DrLA fails to
find a single suggestion. The reason is that cgen finds many counterexamples
to this formula, but it actually does not find any witnesses. In any case, the
conclusion is a disjoint of simple types, so DrLA would be hard-pressed to
find a _simpler_ formula to suggest. It would certainly not even explore terms
with the function symbol append.

The situation is somewhat better in the case of the following theorem:

        (implies (and (not (index-of k x))
                      (index-of k y))
                 (equal (index-of k (append x y))
                        (+ (len x) (index-of k y))))

When DrLA is presented with just the conclusion of this theorem, it discovers
the missing hypotheses (and (not (index-of k x)) (index-of k y)). This reason
this succeeds, is precisely that the key predicate, index-of, appears in the
conclusion of the theorem, so DrLA knows to generate possible hypotheses that
involve index-of.

In contrast, consider the following theorem, also from the standard lists
library:

        (implies (member k x)
                 (equal (nth (index-of k x) x)
                        k))Ψ

DrLA will consider terms that feature the primitive typing predicates, as well
as any functions used in the theorem and the definition of functions that
appear in the theorem, e.g., nth and index-of. However, member does not appear
in the theorem or any of those definitions, so DrLA will fail to suggest the
hypothesis of the theorem. These situations, where the missing hypothesis
requires a predicate that does not otherwise appear in the theorem, are
common.

To address this, DrLA allows the user to provide a list of additional
predicate symbols that it should also consider. If member is provided in this
way, DrLA may suggest (member k x) as a possible missing hypothesis.
Unfortunately, DrLA’s subsumption heuristic leads DrLA astray in this
scenario. The problem is that any term that looks like (or (member k x) P)
subsumes (member k x) regardless of what P is. Thus, DrLA suggests terms like
the following instead of the correct (member k x):

  * •

(or (member k x) (and (rationalp x) (< x 0)))

  * •

(or (complex-rationalp x) (member k x))

But in fact, these weaker hypotheses are not sufficient to prove the theorem;
when x is 1/2, for example, (nth (index-of k x) x) is equal to nil, not
necessarily equal to k. But the reason this shows up as a candidate missing
hypotheses is that the candidates are chosen empirically by examining the
counterexamples and witnesses—not by invoking the theorem prover directly.
What DrLA lacks here is a large enough sample of witnesses and
counterexamples, e.g., at least one counterexample where x is a rational or
complex rational. So DrLA provides the user with 11 total suggestions, though
it does inform the user that only two of them are sufficient to prove the
original theorem, and those two end up being vacuous, i.e., with x=nil.

As these examples make clear, it is vital to the success of DrLA to start with
a suitable set of function symbols so the forest of possible hypotheses is
rich enough to contain useful candidates. Allowing the user to provide some
candidates helps DrLA to succeed in some difficult cases, but it also feels
inappropriate: If the user knows that member is a suitable hypothesis, surely
she can simply provide the necessary hypothesis without using DrLA at all.
This is an open issue that we will return to.

##  4 Implementation Notes

In this section, we describe some of the implementation decisions and
tradeoffs that we encountered implementing DrLA. As previously mentioned, the
first step is to invoke cgen using the function prove/cgen to generate a list
of witnesses and counterexamples, and we ask cgen for 50 of each. If cgen
cannot find any witnesses or any counterexamples, DrLA reports an error and
does not attempt to find missing hypotheses.

Otherwise, DrLA proceeds by generating the expressions that may become
candidate hypotheses. Although there is no such distinction in ACL2, DrLA
considers Boolean patterns, predicates, and terms separately. Boolean patterns
are partial expressions such as

  * •

(or NIL NIL)

  * •

(and (or NIL NIL) NIL)

  * •

(and (not NIL) NIL)

  * •

NIL

The NILs are placeholders where an arbitrary predicate can be placed. These
are just slots; there are no restrictions on the way predicates may appear,
and in particular there is no requirement that the same predicate be used to
replace multiple NILs. Note: The significance of the last template, a single
NIL, will become clear shortly.

DrLA then collects the primitive type predicates (as in the tau system),
essential comparators (such as equal and <<), and any extra predicates
suggested by the user (e.g., member above). Then it generates templates,
similar to the Boolean patterns, using these names. For example, DrLA may
generate terms such as

  * •

(equal NIL NIL)

  * •

(integerp NIL)

  * •

(member NIL NIL)

Unlike the case with the Boolean expressions, DrLA does not nest these
templates, since they are intended to be Booleans that operate on terms.
(Recall that DrLA makes a distinction between Boolean patterns, predicates,
and general terms.) The intent is to avoid considering unpromising expressions
such as (integerp (memberp X (equal Y Z))).

DrLA then combines these two template lists into a single list of templates,
which may include such entries as

  * •

(equal NIL NIL)

  * •

(or (equal NIL NIL) (integerp NIL))

Note that each template is created by replacing one of the NILs in the Boolean
templates by one of the predicate templates (and now the reason for the single
NIL Boolean template should be clear.) There is an exponential explosion here,
so care is taken to use only tail-recursive functions to avoid running out of
stack space. Using DrLA’s default values, the total number of templates formed
at this stage is 2,380—but that number can go up, e.g., if the user specifies
a larger depth for boolean expressions.

Next, DrLA generates the term templates, which are similar to the above, but
based on the functions that are present in the theorem or that appear in the
definitions of those functions, up to a certain depth limit. For example, for
the theorem

        (equal (index-of k (append x y))
               (+ (len x) (index-of k y)))

DrLA will construct terms from the functions APPEND, INDEX-OF, +, CDR, LEN,
and BINARY-+. Thus, it will generate the following 13 templates:

  * •

(+ NIL NIL)

  * •

(append NIL NIL)

  * •

(binary-+ NIL NIL)

  * •

(car NIL)

  * •

(cdr NIL)

  * •

(eqlablep NIL)

  * •

(index-of NIL NIL)

  * •

(index-of-aux NIL NIL NIL)

  * •

(index-of-aux-eq NIL NIL NIL)

  * •

(index-of-aux-eql NIL NIL NIL)

  * •

(len NIL)

  * •

(return-last NIL NIL NIL)

  * •

NIL

In essence, the next step is to combine these templates with each of the 2,380
previously generated templates. However, that would lead to a veritable
explosion of resulting templates, since many of the earlier templates have
more than one placeholder NIL, e.g., the template (or (equal NIL NIL)
(integerp NIL)) which has three NILs, so it would result in $13^{3}=2197$
templates by itself. In a language with lazy evaluation, this would not be a
major problem, but with ACL2 we were concerned about space limitations if we
tried to generate all the templates.

Instead, DrLA proceeds as follows. For each template, it determines how many
placeholders it has, e.g., 3. Then it computes the total number of possible
results, which in this case would be $13^{3}=2197$. Then it uses a counter to
go through all of the possibilities, and generates the corresponding template
just-in-time. E.g., a few of the templates generated may be333In the list, the
numbers refer to the counter in decimal and [base13].)

  * 0.

[000] (or (equal (+ NIL NIL) (+ NIL NIL)) (integerp (+ NIL NIL)))

  * 1.

[001] (or (equal (+ NIL NIL) (+ NIL NIL)) (integerp (append NIL NIL)))

  * 12.

[00c] (or (equal (+ NIL NIL) (+ NIL NIL)) (integerp NIL))

  * 13.

[010] (or (equal (+ NIL NIL) (append NIL NIL)) (integerp (+ NIL NIL)))

The important point is that DrLA does not generate all of these at once.
Rather, it generates the first, fully processes it (as described below), and
then loops to generate the next template.

A further optimization is performed at this stage, which helps to manage the
combinatorial explosion. Consider a term like (and (integerp NIL) (integerp
NIL)). We call these terms redundant, and the key observation is that such a
term was formed from a Boolean template, (and NIL NIL) in this case, and a
predicate, (integerp NIL) in this case. But since NIL is a Boolean template in
its own right, then (integerp NIL) will also be generated as a possible
hypothesis—thus, we can safely ignore the more complicated but logically
equivalent (and (integerp NIL) (integerp NIL)). It’s not just duplicates that
cause this, e.g., consider (and (integerp X) (acl2-numberp X)) where one
subterm implies the other. DrLA recognizes these cases and will ignore any
template with a redundant subterm, since it knows a simpler, equivalent term
will also be considered.

These are still templates, however, not full ACL2 terms. The next step is to
consider the leaves that may be placed in each individual template. These are
the free variables appearing in the original theorem, and possibly444By
default, DrLA does not use the built-in binary predicates equal and <<, in
which case it also does not consider built-in constants. This reflects an
attempt to manage the combinatorial explosion of term generation. a handful of
constants such as 0, 1, t, nil. In our running example, the variables are K,
X, and Y. The final step in term generation is to use these variables and
constants to fill in the placeholders in the templates generated above. Again,
this is done lazily by filling in each template with each possible n-tuple of
values before moving to the next. The resulting terms will include the
following (and many, many more):

  * •

(or (equal (+ X X) (+ X X)) (integerp (+ X X)))

  * •

(or (equal (+ K Y) (+ Y X)) (integerp (+ X K)))

DrLA then processes each term to determine which should be candidate
hypotheses. Recall that DrLA started by gathering a set of counterexamples and
witnesses from cgen. Each counterexample or witness consists of a list of
bindings for the free variables in the original theorem. E.g., a
counterexample may look like

        ((K 3) (X ’(1 2 3)) (Y ’(10 20 30)))

and a witness may look like

        ((K 10) (X ’(1 2 3)) (Y ’(10 20 30)))

The important point is that witnesses and counterexamples fully bind the terms
under consideration, so DrLA can use ACL2’s executable interpreter to
determine the value of each term under that assignment. We use trans-eval for
this purpose, although there are other hooks into the ACL2 interpreter. What
remains, then, is to check if the term evaluates to false for all of the
counterexamples. If that’s the case, then

        (implies TERM
                 BROKEN-THEOREM)

may be an actual theorem, so the term may be a good candidate hypothesis. At
the very least, it eliminates all the (known) counterexamples.

Of course, we want the term to be satisfiable so that adding it as a
hypothesis does not make the final theorem vacuously true. This is where the
witnesses come in. Ideally, the proposed hypothesis will be true for all the
witnesses. Such a hypothesis neatly separates the witnesses from the
counterexamples (always true for the former and false for the latter).

However, we found that this is not always desirable. Our intuition is that
when a user submits a theorem to ACL2, she has an expectation of the types of
the variables under consideration, or some constraint on the possible values
of them. The reason the proof attempt failed, however, is that this
expectation was not explicit in the hypothesis, so the theorem as stated is in
fact false. The counterexamples clearly attest to that, but the witnesses do
not necessarily do the same. For example, consider the (false) theorem

        (equal (<= (* k x) (* k y))
               (<= x y))Ψ

Here, the user forgot to specify that K is a non-negative integer. However,
cgen may find witnesses such as k=-1, x=0, and y=0. In fact, it may find
witnesses such as k=-1, x=NIL, and y=NIL. We call these witnesses, which are
necessarily outside of the user’s intent, “false witnesses.” Insisting that
any proposed hypothesis fully separates the counterexamples from the witnesses
is too strict a requirement in the presence of false witnesses, so DrLA
considers a hypothesis to be a good candidate if it is false for all the
counterexamples, and true for at least one witness.

As mentioned previously, DrLA performs a subsumption check to eliminate as
many candidate hypotheses as possible. The subsumption check is not just
syntactic (as in traditional subsumption) but semantic, since it involves
logical entailment. It would be possible to use the theorem prover itself to
determine this, but we chose not to for two reasons. First, the subsumption
checks happen often, as each potential hypothesis is compared to all other
hypotheses. Making these many calls to the prover may simply prove
impractical. Second, the theorem prover is not complete, so it may fail to
prove that one hypothesis does in fact subsume another. Instead, we chose to
use the witnesses and counterexamples gathered from cgen to test logical
entailment using the executable interpreter in ACL2. The same tradeoff
calculation led to using the interpreter to determine when a template is
redundant, as mentioned previously. Additional experiments are necessary to
determine the right tradeoffs, so these design decisions may change in the
future.

The last step is reporting the final list of candidate hypotheses to the user.
Here, DrLA invokes the theorem prover on each “fixed” theorem, to see which of
the suggested hypotheses in fact succeed in fixing the proofs. DrLA displays
all suggestions to the user, not just the ones that resulted in successful
proof attempts, since the real goal isn’t a “Q.E.D.”, but making explicit the
hidden assumption that the user had forgotten. It may well be that one of the
failing suggestions is actually closer to what the user intended, and seeing
that suggestions will inspire the user to correct the theorem.

##  5 Conclusion and Further Improvements

This paper introduced DrLA, a tool that can help ACL2 users fix broken
theorems by suggesting a forgotten hypothesis. This is done by borrowing and
repurposing ideas from theory exploration and machine learning.

Our experience suggests that DrLA is a promising tool, though more work is
needed before it can reach its potential. Some problems are technological. For
example, since DrLA relies on counterexample generation, it can be only be
used on formulas that are fully executable, i.e., no encapsulates. This
problem may be addressed effectively using defattach.

Other problems are about efficiency. There is a combinatorial explosion at the
heart of DrLA. Computers are getting faster, but combinatorics can’t just be
brushed aside. There are certainly more algorithmic tricks we can use to
reduce the number of templates generated. The reader may have noticed, for
example, that the templates described in Sect. 4 had entries for both + and
binary-+. Detecting such redundancies could result in significant speedups.

Other improvements may come from revisiting DrLA’s heuristics. This is
particularly true of the selection of function names to be used in the term
templates. DrLA looks for function symbols in the theorem itself, and in the
definitions of functions used in the theorem. Some of this is necessary, or
DrLA would only ever be able to suggest simple typing hypotheses. But as the
examples showed, DrLA wastes a lot of time considering possible terms that are
highly improbable, e.g., eqlablep or index-of-aux-eql.

On the other hand, DrLA sometimes fails to find any suitable hypotheses simply
because it does not know to use certain functions. One possible way of
addressing this is to follow the strategy of the tau system, which is to
consider all unary predicates. (It is worth noting that unary predicates are
especially effective at battling the combinatorial problem, since adding a
unary predicate does not change the number of available slots.) However, this
too could result in an excess of templates, since unary predicates are very
common, and DrLA can’t use the greedy optimizations that are so effective in
the tau system. One possibility is to use an explicit system, as in the
defdata types of ACL2. That is something we plan to explore in the near
future. Another possible solution can be found by using machine learning,
which is part of the broader context in which DrLA was developed. In
particular, machine learning could be used to explore the Community Books for
clusters of predicates in hypotheses that are associated with other predicates
in conclusions of theorems. For example, theorems about binary trees may often
use hypotheses about balanced trees. Even if “balanced” is not mentioned in
the conclusion, DrLA could use such information to automatically consider it
in such cases.

Finally, another place where DrLA could be improved is in the interaction with
the counterexample generator. Cgen makes extensive use of the known datatypes
in the way that it searches for counterexamples. For instance, if the formula
contains a variable X that is known to be a binary tree, cgen will try to find
witnesses and counterexamples where X is bound to a binary tree. But this
information is made available to cgen through the related defdata framework,
which not all ACL2 users currently use. Addressing this is a major challenge,
but one that is worthwhile. A better way of finding witnesses and
counterexamples will immediately upgrade DrLA.

DrLA is an ongoing project, and we hope to continue improving it in the near
future by following the roadmap described in this section.

## References

  * [1]
  * [2] ACL2 Documentation (1996): _The Method_.  https://www.cs.utexas.edu/users/moore/acl2/v8-5/combined-manual/?topic=ACL2THE-METHOD.  Accessed: 2023-07-17.
  * [3] ACL2 Documentation (2013): _Introduction to the Tau System_.  https://www.cs.utexas.edu/users/moore/acl2/v8-5/combined-manual/?topic=ACL2INTRODUCTION-TO-THE-TAU-SYSTEM.  Accessed: 2023-07-17.
  * [4] Moa Johansson & Nicholas Smallbone (2021): _Conjectures, Tests and Proofs: An Overview of Theory Exploration_.  Electronic Proceedings in Theoretical Computer Science 341, pp. 1–16, 10.4204/eptcs.341.1.  Available at https://doi.org/10.4204%2Feptcs.341.1.
  * [5] Panagiotis Manolios (2013): _Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities_.  pp. 18–18, 10.1007/978-3-642-39634-24.


* Arcangeli et al. (2017) Arcangeli, L., Borghi, G., Bräuninger, H., et al. 2017, in Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 10565, Proc. SPIE, 1056558
  * Ascenzi et al. (2020) Ascenzi, S., Oganesyan, G., Salafia, O. S., et al. 2020, A&A, 641, A61
  * Bikmaev et al. (2020) Bikmaev, I. F., Irtuganov, E. N., Nikolaeva, E. A., et al. 2020, Astronomy Letters, 46, 645
  * Bleem et al. (2015) Bleem, L. E., Stalder, B., de Haan, T., et al. 2015, ApJS, 216, 27
  * Brunner et al. (2021) Brunner, H., Liu, T., Lamer, G., et al. 2021, arXiv e-prints, arXiv:2106.14517
  * Canalias & Masdemont (2004) Canalias, E. & Masdemont, J. J. 2004, International Astronautical Federation - 55th International Astronautical Congress, 1, 536
  * Castro-Tirado et al. (1992) Castro-Tirado, A. J., Brandt, S., & Lund, N. 1992, IAU Circ., 5590, 2
  * Churazov et al. (1994) Churazov, E., Gilfanov, M., Sunyaev, R., et al. 1994, ApJS, 92, 381
  * Churazov et al. (2021) Churazov, E., Khabibullin, I., Lyskova, N., Sunyaev, R., & Bykov, A. M. 2021, A&A, 651, A41
  * Churazov et al. (2014) Churazov, E., Sunyaev, R., Isern, J., et al. 2014, Nature, 512, 406
  * Churazov et al. (2005) Churazov, E., Sunyaev, R., Sazonov, S., Revnivtsev, M., & Varshalovich, D. 2005, MNRAS, 357, 1377
  * Coutinho et al. (2018) Coutinho, D., Bornemann, W., Budau, B., et al. 2018, in Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 10699, Proc. SPIE, 106995F
  * Dodin et al. (2020) Dodin, A. V., Potanin, S. A., Shatsky, N. I., et al. 2020, Astronomy Letters, 46, 429
  * Doroshenko et al. (2021) Doroshenko, V., Santangelo, A., Tsygankov, S. S., & Ji, L. 2021, A&A, 647, A165
  * Eismont et al. (2020) Eismont, N. A., Kovalenko, I. D., Nazarov, V. N., et al. 2020, Astronomy Letters, 46, 263
  * Freyberg et al. (2020) Freyberg, M., Perinati, E., Pacaud, F., et al. 2020, in Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 11444, Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, 114441O
  * Friedrich et al. (2008) Friedrich, P., Bräuninger, H., Budau, B., et al. 2008, in Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 7011, Proc. SPIE, 70112T
  * Friedrich et al. (2014) Friedrich, P., Rohé, C., Gaida, R., et al. 2014, in Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 9144, Space Telescopes and Instrumentation 2014: Ultraviolet to Gamma Ray, ed. T. Takahashi, J.-W. A. den Herder, & M. Bautz, 91444R
  * Fürmetz et al. (2008) Fürmetz, M., Pfeffermann, E., Predehl, P., Rohé, C., & Tiedemann, L. 2008, in Space Telescopes and Instrumentation 2008: Ultraviolet to Gamma Ray, Vol. 7011, International Society for Optics and Photonics, 70113Y
  * Ghirlanda et al. (2015) Ghirlanda, G., Salvaterra, R., Campana, S., et al. 2015, A&A, 578, A71
  * Gilfanov et al. (1993) Gilfanov, M., Churazov, E., Sunyaev, R., et al. 1993, ApJ, 418, 844
  * Gilfanov et al. (2021) Gilfanov, M., Sazonov, S., Medvedev, P., et al. 2021, The Astronomer’s Telegram, 14800, 1
  * Gilfanov et al. (2020) Gilfanov, M., Sazonov, S., Sunyaev, R., et al. 2020, The Astronomer’s Telegram, 14246, 1
  * Gilfanov et al. (1989) Gilfanov, M., Sunyaev, R., Churazov, E., et al. 1989, Soviet Astronomy Letters, 15, 291
  * Gruber et al. (1999) Gruber, D. E., Matteson, J. L., Peterson, L. E., & Jung, G. V. 1999, ApJ, 520, 124
  * Gubarev et al. (2014) Gubarev, M., Ramsey, B., Kolodziejczak, J. J., et al. 2014, Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 9144, The calibration of flight mirror modules for the ART-XC instrument on board the SRG mission, 91444U
  * Gubarev et al. (2012) Gubarev, M., Ramsey, B., O’Dell, S. L., et al. 2012, Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 8443, The Marshall Space Flight Center development of mirror modules for the ART-XC instrument aboard the Spectrum-Roentgen-Gamma mission, 84431U
  * Haiman et al. (2005) Haiman, Z., Allen, S., Bahcall, N., et al. 2005, arXiv e-prints, astro
  * Hilton et al. (2021) Hilton, M., Sifón, C., Naess, S., et al. 2021, ApJS, 253, 3
  * Hütsi (2006) Hütsi, G. 2006, A&A, 446, 43
  * Jonker et al. (2020) Jonker, P. G., Stone, N. C., Generozov, A., van Velzen, S., & Metzger, B. 2020, ApJ, 889, 166
  * Kardashev et al. (2013) Kardashev, N. S., Khartov, V. V., Abramov, V. V., et al. 2013, Astronomy Reports, 57, 153
  * Kawamuro et al. (2018) Kawamuro, T., Ueda, Y., Shidatsu, M., et al. 2018, ApJS, 238, 32
  * Khabibullin et al. (2020a) Khabibullin, I., Medvedev, P., Churazov, E., et al. 2020a, The Astronomer’s Telegram, 13499, 1
  * Khabibullin et al. (2016) Khabibullin, I., Medvedev, P., & Sazonov, S. 2016, MNRAS, 455, 1414
  * Khabibullin et al. (2012) Khabibullin, I., Sazonov, S., & Sunyaev, R. 2012, MNRAS, 426, 1819
  * Khabibullin et al. (2014) Khabibullin, I., Sazonov, S., & Sunyaev, R. 2014, MNRAS, 437, 327
  * Khabibullin et al. (2020b) Khabibullin, I., Sunyaev, R., Churazov, E., et al. 2020b, The Astronomer’s Telegram, 13494, 1
  * Khorunzhev et al. (2020) Khorunzhev, G. A., Meshcheryakov, A. V., Burenin, R. A., et al. 2020, Astronomy Letters, 46, 149
  * Khorunzhev et al. (2021) Khorunzhev, G. A., Meshcheryakov, A. V., Medvedev, P. S., et al. 2021, Astronomy Letters, 47, 123
  * Krivonos et al. (2017) Krivonos, R., Tkachenko, A., Burenin, R., et al. 2017, Experimental Astronomy, 44, 147
  * Lamer et al. (2021) Lamer, G., Schwope, A. D., Predehl, P., et al. 2021, A&A, 647, A7
  * Levin et al. (2014) Levin, V., Pavlinsky, M., Akimov, V., et al. 2014, Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 9144, ART-XC/SRG: status of the x-ray focal plane detector development, 914413
  * Levin et al. (2016) Levin, V., Pavlinsky, M., Akimov, V., et al. 2016, Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 9905, Results of ground tests and calibration of x-ray focal plane detectors for ART-XC/SRG instrument, 990551
  * Liu et al. (2021) Liu, Z., Rau, A., Malyali, A., Merloni, A., & Grotova, I. 2021, The Astronomer’s Telegram, 14407, 1
  * Lumb et al. (2002) Lumb, D. H., Warwick, R. S., Page, M., & De Luca, A. 2002, A&A, 389, 93
  * Lutovinov et al. (2021) Lutovinov, A. A., Tsygankov, S. S., Mereminskiy, I. A., et al. 2021, arXiv e-prints, arXiv:2107.05587
  * Malyali et al. (2019) Malyali, A., Rau, A., & Nandra, K. 2019, MNRAS, 489, 5413
  * Medvedev et al. (2021) Medvedev, P., Gilfanov, M., Sazonov, S., Schartel, N., & Sunyaev, R. 2021, MNRAS, 504, 576
  * Medvedev et al. (2020) Medvedev, P., Sazonov, S., Gilfanov, M., et al. 2020, MNRAS, 497, 1842
  * Meidinger et al. (2014) Meidinger, N., Andritschke, R., Bornemann, W., et al. 2014, in Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, Vol. 9144, Proc. SPIE, 91441W
  * Mereminskiy et al. (2020a) Mereminskiy, I., Lutovinov, A., Semena, A., et al. 2020a, The Astronomer’s Telegram, 14051, 1
  * Mereminskiy et al. (2020b) Mereminskiy, I., Medvedev, P., Lutovinov, A., et al. 2020b, The Astronomer’s Telegram, 14206, 1
  * Mereminskiy et al. (2020c) Mereminskiy, I., Medvedev, P., Semena, A., et al. 2020c, The Astronomer’s Telegram, 13571, 1
  * Mereminskiy et al. (2020d) Mereminskiy, I., Semena, A., Pavlinsky, M., et al. 2020d, The Astronomer’s Telegram, 13606, 1
  * Mereminskiy et al. (2021) Mereminskiy, I. A., Dodin, A. V., Lutovinov, A. A., et al. 2021, arXiv e-prints, arXiv:2107.05588
  * Merloni et al. (2012) Merloni, A., Predehl, P., Becker, W., et al. 2012, arXiv e-prints, arXiv:1209.3114
  * Pavlinsky et al. (2021a) Pavlinsky, M., Sazonov, S., Burenin, R., et al. 2021a, arXiv e-prints, arXiv:2107.05879
  * Pavlinsky et al. (2021b) Pavlinsky, M., Tkachenko, A., Levin, V., et al. 2021b, A&A, 650, A42
  * Pavlinsky et al. (2019a) Pavlinsky, M., Tkachenko, A., Levin, V., et al. 2019a, Experimental Astronomy, 48, 233
  * Pavlinsky et al. (2018) Pavlinsky, M., Tkachenko, A., Levin, V., et al. 2018, Experimental Astronomy, 45, 315
  * Pavlinsky et al. (2019b) Pavlinsky, M., Tkachenko, A., Levin, V., et al. 2019b, Experimental Astronomy, 47, 1
  * Pavlinsky et al. (1994) Pavlinsky, M. N., Grebenev, S. A., & Sunyaev, R. A. 1994, ApJ, 425, 110
  * Pavlinsky et al. (2020) Pavlinsky, M. N., Tkachenko, A. Y., Levin, V. V., et al. 2020, Instruments and Experimental Techniques, 63, 243
  * Peebles & Yu (1970) Peebles, P. J. E. & Yu, J. T. 1970, ApJ, 162, 815
  * Planck Collaboration et al. (2013) Planck Collaboration, Ade, P. A. R., Aghanim, N., et al. 2013, A&A, 554, A140
  * Planck Collaboration et al. (2016) Planck Collaboration, Ade, P. A. R., Aghanim, N., et al. 2016, A&A, 594, A27
  * Predehl et al. (2021) Predehl, P., Andritschke, R., Arefiev, V., et al. 2021, A&A, 647, A1
  * Predehl et al. (2020) Predehl, P., Sunyaev, R. A., Becker, W., et al. 2020, Nature, 588, 227
  * Reiprich et al. (2021) Reiprich, T. H., Veronica, A., Pacaud, F., et al. 2021, A&A, 647, A2
  * Revnivtsev et al. (2009) Revnivtsev, M., Sazonov, S., Churazov, E., et al. 2009, Nature, 458, 1142
  * Saxton et al. (2008) Saxton, R. D., Read, A. M., Esquej, P., et al. 2008, A&A, 480, 611
  * Sazonov et al. (2020) Sazonov, S., Burenin, R., Khorunzhev, G., et al. 2020, The Astronomer’s Telegram, 13987, 1
  * Sazonov et al. (2021) Sazonov, S., Gilfanov, M., Medvedev, P., et al. 2021, arXiv e-prints, arXiv:2108.02449
  * Schuecker et al. (2003) Schuecker, P., Böhringer, H., Collins, C. A., & Guzzo, L. 2003, A&A, 398, 867
  * Schwope et al. (2021) Schwope, A., Buckley, D. A. H., Kawka, A., et al. 2021, arXiv e-prints, arXiv:2106.14538
  * Schwope et al. (2020) Schwope, A., Semena, A., Maitra, C., et al. 2020, The Astronomer’s Telegram, 14219, 1
  * Snowden et al. (1997) Snowden, S. L., Egger, R., Freyberg, M. J., et al. 1997, ApJ, 485, 125
  * Strüder et al. (2001) Strüder, L., Briel, U., Dennerl, K., et al. 2001, A&A, 365, L18
  * Sunyaev et al. (1987) Sunyaev, R., Kaniovsky, A., Efremov, V., et al. 1987, Nature, 330, 227
  * Sunyaev et al. (1991) Sunyaev, R. A., Aref’ev, V., Borozdin, K., et al. 1991, Advances in Space Research, 11, 5
  * Sunyaev et al. (1993) Sunyaev, R. A., Markevitch, M., & Pavlinsky, M. 1993, ApJ, 407, 606
  * Sunyaev & Zeldovich (1980) Sunyaev, R. A. & Zeldovich, I. B. 1980, ARA&A, 18, 537
  * Sunyaev & Zeldovich (1970) Sunyaev, R. A. & Zeldovich, Y. B. 1970, Ap&SS, 7, 3
  * Syunyaev et al. (1991) Syunyaev, R. A., Arefev, V. A., Borozdin, K. N., et al. 1991, Soviet Astronomy Letters, 17, 409
  * Syunyaev et al. (1994) Syunyaev, R. A., Borozdin, K. N., Aleksandrovich, N. L., et al. 1994, Astronomy Letters, 20, 777
  * Syunyaev et al. (1987) Syunyaev, R. A., Kaniovskii, A., Efremov, V., et al. 1987, Soviet Astronomy Letters, 13, 431
  * Tkachenko et al. (2002) Tkachenko, A. Y., Terekhov, O. V., Sunyaev, R. A., et al. 2002, Astronomy Letters, 28, 353
  * Trümper (1982) Trümper, J. 1982, Advances in Space Research, 2, 241
  * Vainshtein & Syunyaev (1980) Vainshtein, L. A. & Syunyaev, R. A. 1980, Soviet Astronomy Letters, 6, 353
  * Voges et al. (1999) Voges, W., Aschenbach, B., Boller, T., et al. 1999, A&A, 349, 389
  * Wilms et al. (2020) Wilms, J., Kreykenbohm, I., Weber, P., et al. 2020, The Astronomer’s Telegram, 13416, 1
  * Wolf et al. (2021) Wolf, J., Nandra, K., Salvato, M., et al. 2021, A&A, 647, A5
  * Wolter (1952a) Wolter, H. 1952a, Annalen der Physik, 445, 94
  * Wolter (1952b) Wolter, H. 1952b, Annalen der Physik, 445, 286
  * Yao et al. (2020a) Yao, Y., Kulkarni, S. R., Burdge, K. B., et al. 2020a, arXiv e-prints, arXiv:2012.00169
  * Yao et al. (2020b) Yao, Y., Kulkarni, S. R., Gendreau, K. C., et al. 2020b, arXiv e-prints, arXiv:2012.00160
  * Zaznobin et al. (2021a) Zaznobin, I., Sazonov, S., Burenin, R., et al. 2021a, arXiv e-prints, arXiv:2107.05611
  * Zaznobin et al. (2021b) Zaznobin, I. A., Uskov, G. S., Sazonov, S. Y., et al. 2021b, Astronomy Letters, 47, 89