=Paper=
{{Paper
|id=Vol-3009/short2
|storemode=property
|title=SEH-PILoT: A System for Property-Directed Symbol Elimination – Work in Progress (Short Paper)
|pdfUrl=https://ceur-ws.org/Vol-3009/short2.pdf
|volume=Vol-3009
|authors=Philipp Marohn,Viorica Sofronie-Stokkermans
|dblpUrl=https://dblp.org/rec/conf/kr/MarohnS21
}}
==SEH-PILoT: A System for Property-Directed Symbol Elimination – Work in Progress (Short Paper)==
https://ceur-ws.org/Vol-3009/short2.pdf
SEH-PILoT: A System for Property-Directed
Symbol Elimination – Work in Progress
(Short Paper)
Philipp Marohn and Viorica Sofronie-Stokkermans
University Koblenz-Landau, Koblenz, Germany
{pmarohn,sofronie}@uni-koblenz.de
Abstract. We describe the implementation of a system for property-
directed symbol elimination in extensions of a theory T0 with additional
function symbols whose properties are axiomatised using a set of clauses.
The system performs the symbol elimination in a hierarchical way, relying
on existing mechanisms for symbol elimination in T0 .
1 Introduction
Many reasoning problems in mathematics or program verification can be reduced
to checking satisfiability of ground formulae w.r.t. a theory (this can be a stan-
dard theory, e.g. linear arithmetic, or a complex theory – e.g. the extension of a
base theory with additional function symbols axiomatized by a set of formulae,
or a combination of theories). More interesting is to go beyond yes/no answers,
i.e. to consider problems – in mathematics or verification – in which the proper-
ties of certain function symbols are underspecified (these symbols are considered
to be parametric) and (weakest) additional conditions need to be derived under
which given properties hold. In [13] a method for property-directed symbol elim-
ination in local theory extensions was proposed which can be used for obtaining
such constraints on parameters. The goal of this paper is to present the current
state of an implementation of this method in the system SEH-PILoT.
Structure of the paper: In Section 2.2 we first present the theoretical background
and then the implementation details. In Section 3 we discuss in detail an example,
then present an overview of a (small) subset of the tests we considered so far.
2 Description of the SEH-PILoT Implementation
SEH-PILoT (Symbol Elimination based on Hierarchical Proving In Local Theory
extensions) is an implementation of the method for symbol elimination presented
in [12,13]. SEH-PILoT is implemented in Python 3.9. Its general structure is
presented in Figure 1. Examples which show how SEH-PILoT can be used in
various application areas (mathematics, verification, wireless network theory)
can be found at https://userpages.uni-koblenz.de/~sofronie/sehpilot/.
Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
76 Philipp Marohn and Viorica Sofronie-Stokkermans
2.1 Theoretical Background
Let Π0 =(Σ0 , Pred) be a signature, and T0 be a “base” theory with signature Π0 .
We consider extensions T := T0 ∪K of T0 with new function symbols Σ (extension
functions) whose properties are axiomatized using a set K of (universally closed)
clauses in the extended signature Π = (Σ0 ∪ Σ, Pred), such that each clause in
K contains function symbols in Σ. Let Σpar ⊆ Σ be a set of parameters. Let Σc
be an additional set of constants.
Task: Let G be a set of ground Π ∪ Σc clauses. We want to check whether G is
satisfiable w.r.t. T0 ∪ K or not and – if it is satisfiable – to generate a weakest
universal Π0 ∪ Σpar -formula Γ such that T0 ∪ K ∪ Γ ∪ G is unsatisfiable.
Method. For satisfiability checking we use a method for hierarchical reduc-
tion to checking satisfiability in the base theory. For symbol elimination (i.e. for
determining Γ ) we use a method for hierarchically reducing the problem to a
quantifier elimination problem w.r.t. T0 . If T0 allows quantifier elimination (i.e.
for every formula φ over Π0 there exists a quantifier-free formula φ∗ over Π0
which is equivalent to φ modulo T0 ) a method for quantifier elimination w.r.t.
T0 can be used for this.
In what follows we present situations in which hierarchical reasoning is complete
and weakest constraints on parameters can be generated.
Local Theory Extensions. Let Ψ be a closure operator on sets of ground
terms. A theory extension T0 ⊆ T0 ∪ K is Ψ -local if it satisfies the condition:
Ψ
(Locf ) For every finite set G of ground Π C -clauses (for an additional
set C of constants) it holds that T0 ∪ K ∪ G |= ⊥ if and only if
T0 ∪ K[ΨK (G)] ∪ G is unsatisfiable.
where, for every set G of ground Π C -clauses, K[ΨK (G)] is the set of instances
of K in which the terms starting with a function symbol in Σ are in ΨK (G) =
Ψ (est(K, G)), where est(K, G) is the set of ground terms starting with a function
in Σ occurring in G or K.
Ψ -local extensions can be recognized by showing that certain partial models
embed into total ones [11,7]. Especially well-behaved are theory extensions with
the property (CompΨ f ) which requires that every partial model of T whose reduct
to Π0 is total and the “set of defined terms” is finite and closed under Ψ , embeds
into a total model of T with the same support (cf. e.g. [5]). If Ψ is the identity, we
denote LocΨ Ψ
f by Locf and Compf by Compf . Examples of local theory extensions
can be found in [14].
Hierarchical Reasoning. Consider a Ψ -local theory extension T0 ⊆ T0 ∪ K.
Condition (LocΨ
f ) requires that for every finite set G of ground Π
C
clauses: T0 ∪
K∪G |=⊥ if and only if T0 ∪K[ΨK (G)]∪G |=⊥ . In all clauses in K[ΨK (G)]∪G the
function symbols in Σ only have ground terms as arguments, so K[ΨK (G)]∪G
can be flattened and purified1 by introducing, in a bottom-up manner, new
1
i.e. the function symbols in Σ are separated from the other symbols.
SEH-PILoT 77
constants ct ∈ C for subterms t=f (c1 , . . . , cn ) where f ∈Σ and ci are constants,
together with definitions ct ≈f (c1 , . . . , cn ) which are all included in a set Def.
We thus obtain a set of clauses K0 ∪G0 ∪Def, where K0 and G0 do not contain
Σ-function symbols and Def contains clauses of the form c≈f (c1 , . . . , cn ), where
f ∈Σ, c, c1 , . . . , cn are constants.
Theorem 1 ([11,5]) Let K be a set of clauses. Assume that T0 ⊆ T1 = T0 ∪K is
a Ψ -local theory extension. For any finite set G of ground clauses, let K0 ∪G0 ∪Def
be obtained from K[ΨK (G)]∪G by flattening and purification, as explained above.
Then the following are equivalent to T1 ∪ G |=⊥:
(1) T0 ∪K[ΨK (G)]∪G |=⊥ .
n
^ f (c1 , . . . , cn )≈c∈Def
(2) T0 ∪K0 ∪G0 ∪Con0 |=⊥, where Con0 ={ ci ≈di → c≈d | }.
f (d1 , . . . , dn )≈d∈Def
i=1
We can also consider chains of theory extensions:
T0 ⊆ T1 = T0 ∪ K1 ⊆ T2 = T0 ∪ K1 ∪ K2 ⊆ · · · ⊆ Tn = T0 ∪ K1 ∪ ... ∪ Kn
in which each theory is a local extension of the preceding one. For a chain of
n local extensions a satisfiability check w.r.t. the last extension can be reduced
(in n steps) to a satisfiability check w.r.t. T0 . The only restriction we need to
impose in order to ensure that such a reduction is possible is that at each step
the clauses reduced so far need to be ground. Groundness is assured if each
variable in a clause appears at least once under an extension function. This
iterated instantiation procedure for chains of local theory extensions has been
implemented in H-PILoT [6].2
Hierarchical Symbol Elimination. In [13] we proposed a method for property-
directed symbol elimination described in Algorithm 1.
Theorem 2 ([12,13]) Let T0 be a Π0 -theory allowing quantifier elimination,
Σpar be a set of parameters (function and constant symbols) and Σ a set of
function symbols such that Σ ∩ (Σ0 ∪ Σpar ) = ∅. Let K be a set of clauses in the
signature Π0 ∪Σpar ∪Σ in which all variables occur also below functions in Σ1 =
Σpar ∪ Σ. Assume T ⊆ T0 ∪ K satisfies condition (CompΨ f ) for a suitable closure
operator Ψ . Let T = ΨK (G). Then Algorithm 1 yields a universal Π0 ∪ Σpar -
formula ∀x. ΓT (x) such that T0 ∪ ∀x. ΓT (x) ∪ K ∪ G |=⊥ which is entailed by
every universal formula Γ with T0 ∪ Γ ∪ K ∪ G |=⊥.
Algorithm 1 yields a formula ∀x. ΓT (x) with T0 ∪ ∀x. ΓT (x) ∪ K ∪ G |=⊥ also if
the extension T ⊆ T0 ∪ K is not Ψ -local or T 6= ΨK (G), but in this case there is
no guarantee that ∀x. ΓT (x) is the weakest universal formula with this property.
A similar result holds for chains of local theory extensions.
2
H-PILoT allows the user to specify a chain of extensions by tagging the extension
functions with their place in the chain (e.g., if f occurs in K3 but not in K1 ∪ K2 it
is declared as level 3).
78 Philipp Marohn and Viorica Sofronie-Stokkermans
Algorithm 1 Symbol elimination in theory extensions [12,13]
Input: Theory extension T0 ∪ K with signature Π = Π0 ∪ (Σ ∪ Σpar )
where Σpar is a set of parameters
Set T of ground Π C -terms
Output: ∀y. ΓT (y) (universal Π0 ∪ Σpar -formula)
Step 1 Purify K[T ] ∪ G as described in Theorem 1 (with set of extension symbols Σ1 ).
Let K0 ∪ G0 ∪ Con0 be the set of Π0C -clauses obtained this way.
Step 2 Let G1 = K0 ∪ G0 ∪ Con0 . Among the constants in G1 , we identify
(i) the constants cf , f ∈ Σpar , where cf is a constant parameter or cf is introduced
by a definition cf ≈ f (c1 , . . . , ck ) in the hierarchical reasoning method,
(ii) all constants cp occurring as arguments of functions in Σpar in such definitions.
Replace all the other constants c with existentially quantified variables x (i.e.
replace G1 (cp , cf , c) with ∃x. G1 (cp , cf , x)).
Step 3 Construct a formula Γ1 (cp , cf ) equivalent to ∃x. G1 (cp , cf , x) w.r.t. T0 using a
method for quantifier elimination in T0 and let Γ2 (cp , cf ) be ¬Γ1 (cp , cf ).
Step 4 Replace (i) each constant cf introduced by definition cf ≈ f (c1 , . . . , ck )
with the term f (c1 , . . . , ck ) and (ii) cp with universally quantified variables y in
Γ2 (cp , cf ). The formula obtained this way is ∀y. ΓT (y).
Theorem 3 ([13]) Consider the following chain of theory extensions:
T0 ⊆ T0 ∪ K1 ⊆ T0 ∪ K1 ∪ K2 ⊆ . . . ⊆ T0 ∪ K1 ∪ K2 ∪ · · · ∪ Kn
where every extension in the chain satisfies condition (Compf ), Ki are all flat
and linear, and in all Ki all variables occur below the extension terms on level i.
Let G be a set of ground clauses, and let G1 be the result of the hierarchical
reduction of satisfiability of G to a satisfiability test w.r.t. T0 . Let T = T (G)
be the set of all instances used in the chain of hierarchical reductions and let
∀y. ΓT (G) (y) be the formula obtained by applying Steps 2–4 of Alg. 1 to G1 . Then
∀y. ΓT (G) (y) is entailed by every conjunction Γ of clauses with the property that
T0 ∪ Γ ∪ K1 ∪ · · · ∪ Kn ∪ G is unsatisfiable (i.e. it is the weakest such constraint).
2.2 Implementation
Hierarchical reasoning: H-PILoT. The method for hierarchical reasoning in
local theory extensions described before was implemented in the system H-PILoT
[6]. H-PILoT carries out a hierarchical reduction to the base theory. Standard
SMT provers or specialized provers can be used for testing the satisfiability of the
formulae obtained after the reduction. H-PILoT uses eager instantiation and the
hierarchical reduction, so provers like CVC4 [1] or Z3 [2] are in general faster
in proving unsatisfiability. The advantage of using H-PILoT is that knowing
the instances needed for a complete instantiation allows us to correctly detect
satisfiability (and generate models) in situations in which e.g. CVC4 returns
“unknown”, and use property-directed symbol elimination to obtain additional
constraints on parameters which ensure unsatisfiability.
SEH-PILoT 79
Symbol Elimination: SEH-PILoT (Symbol Elimination with H-PILoT):
For obtaining constraints on parameters we used the method described in Al-
gorithm 1 [13] which was implemented in SEH-PILoT for the case in which
the theory can be structured as a local theory extension or a chain of theory
extensions and the base theory T0 is the theory of real closed fields.
Input. SEH-PILoT receives a list of symbols to be eliminated (and possibly
a list of already existing constraints on the parameters) and an input file for
H-PILoT3 . This file contains (i) the specification of the signature and of the
hierarchy of local theory extensions to be considered; (ii) an axiomatization K
of the theory extension(s); (iii) a set G of ground clauses possibly containing
additional constants. Currently the only supported base theory for SEH-PILoT
is the theory of real numbers (the theory of real closed fields).
Main Algorithm. SEH-PILoT follows the steps of Algorithm 1.
Step 1: SEH-PILoT uses H-PILoT (with op-
tion -redlog) for the hierarchical reduction to
a problem in the base theory. H-PILoT com-
putes the necessary instances K[TG ], where TG
is the set of ground terms necessary for in-
stantiation (cf. Thm.3), generates the formula
K0 ∪ G0 ∪ Con0 and writes it in a file which can
be used as input for Redlog [4].
Step 2: Taking into account the function sym-
bols to be eliminated, the constants are clas-
sified as required in Step 2 of Alg. 1 and the
Redlog file is changed accordingly such that
only those symbols that do not correspond to
a parameter or argument of a parameter are
considered to be existentially quantified.
Step 3: SEH-PILoT uses Redlog to eliminate
the existentially quantified symbols and after-
wards to negate the resulting formula.
Step 4: The constants contained in the formula
obtained by Step 3 are replaced back with the
terms they represent and the constants occur-
ring as arguments are replaced by universally
quantified variables. Fig. 1. SEH-PILoT structure
Finally SEH-PILoT translates the generated
constraints from the syntax of Redlog back to the syntax of H-PILoT such that
they can easily be used for verification or an iterative approach of constraint
generation. Since Redlog is not very efficient in simplifying formulae, SLFQ can
be used, which allows Redlog to use the possibilities of simplification offered by
QEPCAD B [3].
3
A detailed description of the form of such input files can be found in the system
description of H-PILoT [6].
80 Philipp Marohn and Viorica Sofronie-Stokkermans
3 Examples
We illustrate the way SEH-PILoT works on the following example4 . Consider a
discrete water level controller in which the inflow varies during the evolution of
the system, and can be modeled by a function inflow : R → R, where inflow(t)
is the inflow at time step t. If the water level becomes greater than an alarm
level Lalarm (positioned below the overflow level Loverflow ) a valve is opened and a
fixed quantity of water (outflow) is left out. Otherwise, the valve remains closed.
Assume that the formula Init(L) := L Loverflow );
(2) ∃L, L0 , t, t0 . (L≤Loverflow ∧L>Lalarm ∧L0 ≈L+inflow(t)−outflow∧t0 ≈t+1∧L0 >Loverflow );
(3) ∃L, L0 , t, t0 . (L≤Loverflow ∧ L≤Lalarm ∧ L0 ≈L+inflow(t) ∧ t0 ≈t+1 ∧ L0 >Loverflow ).
We want to obtain conditions on the parameters (inflow, outflow, Lalarm , Loverflow )
under which L < Loverflow is an inductive invariant. (1) is clearly unsatisfiable.
SEH-PILoT (with assumptions Lalarm < Loverflow , ∀x. inflow(x) > 0) generated
weakest universal conditions under which (2) resp. (3) are unsatisfiable. Consider
e.g. (2). The problem is described in the H-PILoT syntax as follows:
B a s e f u n c t i o n s :={(+ ,2) , ( − ,2) , ( ∗ , 2 ) }
E x t e n s i o n f u n c t i o n s :={( i n f l o w , 1 , 1)}
R e l a t i o n s :={(<=, 2 ) , ( < , 2 ) , (>=, 2 ) , ( > , 2 ) }
C l a u s e s := l <= l o v e r f l o w ; l > l a l a r m ; l p = ( l+i n f l o w ( t )) − o u t f l o w ; tp = t+ 1 ;
Query := lp > loverflow ;
It can be checked that the extension R ⊆ R∪K of R with a function symbol inflow
satisfying the axiom K = ∀x.(inflow(x) > 0) defines a local theory extension.
When using SEH-PILoT the user has to specify the name of the H-PILoT file (in
this case inv2.loc), the symbols to be eliminated (l, lp and tp) and any addi-
tional constraints on the parameters (lalarm0)).
This is done in the command line:
sehpilot inv2.loc -e l lp tp -a ’lalarm0’ --stats
If called with the additional constraints added to the command line (example
“Water tank, -a” in Table 1) SEH-PILoT generates the right instances. Alter-
natively, the clause ∀x.(inflow(x) > 0) can be added to the Clauses in the
inv2.loc-file (example “Water tank, no -a” in Table 1). In both cases H-PILoT
performs the hierarchical reduction described in Theorem 1 for G being the
conjunction of the ground formulae in Clauses, Query and in the additional as-
sumptions if option -a is used, by determining the set T = est(G) = {inflow(t)}
of terms in G starting with an extension function, considering the instances of
K containing this term, K[T ] = {inflow(t) > 0} and introducing a constant e1
for inflow(t), and generates the Redlog file:
4
This example as well as several additional examples can be found under https:
//userpages.uni-koblenz.de/~sofronie/sehpilot/.
SEH-PILoT 81
load package redlog ; r l s e t OFSF ; off r l v e r b o s e ; on r l n z d e n ; o f f nat ;
vars := { l a l a r m , e 1 , l , l p , o u t f l o w , l o v e r f l o w , t , tp } ;
f o r m u l a := ( l p > l o v e r f l o w and l > l a l a r m and l <= l o v e r f l o w and
tp = t + 1 and l p = ( l + e1 ) − o u t f l o w ) ;
q u e r y := ( r l q e ex ( v a r s , f o r m u l a ) ) ; end ;
SEH-PILoT classifies the constants and updates the Redlog file by simplifying
the input and changing vars to the set of symbols to be eliminated l, lp, tp,
eliminates these variables, negates the result and simplifies5 the resulting formula
and obtains e1 − outflow ≤ 0. It then replaces e1 with inflow(t), quantifies t
universally and obtains the weakest constraint:
(Γ1 ) ∀t. (inflow(t) ≤ outflow)
for which (2) becomes unsatisfiable. A similar procedure yields the constraint
(Γ2 ) ∀t. (lalarm + inflow(t) ≤ loverflow) for (3).
Test runs for SEH-PILoT. We analyzed examples from mathematics, verifi-
cation and wireless network theory. We used H-PILoT for testing satisfiability
of the formulae; if the formulae were satisfiable SEH-PILoT was used for symbol
elimination and generating constraints on the parameters. The table below pro-
vides some data on the size of the problems we analyzed and the time H-PILoT
needed for hierarchical reduction and SEH-PILoT for symbol elimination.
Name # clauses time H-PILoT # atoms # atoms time QE # atoms # atoms Time
input (s) (1) (2) (ms) (3) (4) (s)
Mathematics
Case distinction 4 0.23 16 12 0.81 34 8 2.5
Example 5.6 in [13]
Lipschitz 12 0.25 64 22 5.26 2925 3 9.5
Verification
Water tank, -a 7 0.22 5 5 0.19 2 2 1.7
without SLFQ
Water tank, no -a 6 0.10 6 6 0.08 2 2 0.8
without SLFQ
Array sorted 6 0.23 11 8 0.82 2 2 2.5
Example 4 in [9]
Maximum in array 7 0.22 11 6 0.8 1 1 3.0
Example 4.13 [14]
Networks
Graph class consist. 3 0.22 3 3 0.79 1 1 2.4
Example 4 in [10]
Class inclusion (g4 ) 19 0.24 111 22 0.90 20 4 2.5
Class inclusion (g5 ) 19 0.24 114 22 1.01 20 4 2.7
Example 8 in [10,8]
Table 1. Run on an Intel(R) Core(TM) i7-3770 CPU @ 3.40GHz, 8192 K-byte cache.
# clauses is the number of clauses in the input to H-PILoT. # atoms refer to the number of atoms
in the Redlog file generated by H-PILoT before (1) resp. after (2) simplification; resp. in the formu-
la obtained after quantifier elimination before (3) resp. after (4) simplification.
For all examples (with exception of the water tank) simplification with SLFQ was used, which is
responsible for a significant amount of the runtime.
5
If SEH-PILoT is called with assumptions (-a) in the command line, redlog-
simplification with assumptions is performed and the resulting formula is simpler.
82 Philipp Marohn and Viorica Sofronie-Stokkermans
References
1. C. W. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King,
A. Reynolds, and C. Tinelli. CVC4. In G. Gopalakrishnan and S. Qadeer, ed-
itors, Computer Aided Verification - 23rd International Conference, CAV 2011,
Proceedings, LNCS 6806, pages 171–177. Springer, 2011.
2. N. Bjørner, L. de Moura, L. Nachmanson, and C. M. Wintersteiger. Programming
Z3. In J. P. Bowen, Z. Liu, and Z. Zhang, editors, Engineering Trustworthy Software
Systems - 4th International School, SETSS 2018, Tutorial Lectures, LNCS 11430,
pages 148–201. Springer, 2019.
3. C. W. Brown. QEPCAD B: a system for computing with semi-algebraic sets via
cylindrical algebraic decomposition. SIGSAM Bull., 38(1):23–24, 2004.
4. A. Dolzmann and T. Sturm. REDLOG: computer algebra meets computer logic.
SIGSAM Bull., 31(2):2–9, 1997.
5. C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans. On local reasoning in ver-
ification. In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for
the Construction and Analysis of Systems, 14th International Conference, TACAS
2008, Proceedings, LNCS 4963, pages 265–281. Springer, 2008.
6. C. Ihlemann and V. Sofronie-Stokkermans. System description: H-PILoT. In R. A.
Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference
on Automated Deduction, Proceedings, LNCS 5663, pages 131–139. Springer, 2009.
7. C. Ihlemann and V. Sofronie-Stokkermans. On hierarchical reasoning in combi-
nations of theories. In J. Giesl and R. Hähnle, editors, Automated Reasoning,
5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages
30–45. Springer, 2010.
8. D. Peuter, P. Marohn, and V. Sofronie-Stokkermans. Symbol elimination for para-
metric second-order entailment problems (with applications to problems in wireless
network theory). CoRR, https://arxiv.org/abs/2107.02333, 2021.
9. D. Peuter and V. Sofronie-Stokkermans. On invariant synthesis for parametric
systems. In P. Fontaine, editor, Automated Deduction - CADE 27 - 27th Inter-
national Conference on Automated Deduction, Proceedings, LNCS 11716, pages
385–405. Springer, 2019.
10. D. Peuter and V. Sofronie-Stokkermans. Symbol elimination and applications to
parametric entailment problems. In B. Konev and G. Reger, editors, Frontiers of
Combining Systems - 13th International Symposium, FroCoS 2021, Proceedings,
LNCS 12941, pages 43–62. Springer, 2021.
11. V. Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In
R. Nieuwenhuis, editor, Automated Deduction - CADE-20, 20th International
Conference on Automated Deduction, Proceedings, LNCS 3632, pages 219–234.
Springer, 2005.
12. V. Sofronie-Stokkermans. On interpolation and symbol elimination in theory ex-
tensions. In N. Olivetti and A. Tiwari, editors, Automated Reasoning - 8th Inter-
national Joint Conference, IJCAR 2016, Proceedings, LNCS 9706, pages 273–289.
Springer, 2016.
13. V. Sofronie-Stokkermans. On interpolation and symbol elimination in theory ex-
tensions. Log. Methods Comput. Sci., 14(3), 2018.
14. V. Sofronie-Stokkermans. Parametric systems: Verification and synthesis. Fundam.
Informaticae, 173(2-3):91–138, 2020.